HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem sylanb 449
Description: A syllogism inference.
Hypotheses
Ref Expression
sylan.1 |- ((ph /\ ps) -> ch)
sylanb.2 |- (th <-> ph)
Assertion
Ref Expression
sylanb |- ((th /\ ps) -> ch)
Proof of Theorem sylanb
StepHypRef Expression
1 sylan.1 . 2 |- ((ph /\ ps) -> ch)
2 sylanb.2 . . 3 |- (th <-> ph)
32biimp 151 . 2 |- (th -> ph)
41, 3sylan 448 1 |- ((th /\ ps) -> ch)
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223
This theorem is referenced by:  syl2anb 455  2euex 1439  2exeu 1444  eqtr2t 1490  sspsstr 2147  disjne 2311  ordon 2982  ordsucss 3064  ordsucelsuc 3068  funex 3600  fssres 3634  fvimacnvi 3795  tz7.48lem 3946  1st2nd 4098  oeworde 4210  nnmsucr 4230  erref 4265  mapxpen 4481  php 4499  php3 4501  php4 4502  omsucdom 4508  isfinite2 4529  fodomfi 4546  brdom3 4781  cfeq0 4894  pre-axsup 5271  divmul13t 5746  lemuldivt 5832  uzindOLD 6164  qbtwnxr 6225  faclbnd 6890  faclbnd3 6892  fsum0clt 6962  ser0clt 6992  ser1clt 6993  binomlem5 7016  climaddlem3 7060  climmullem8 7071  climcmplem 7081  isumnn0nna 7151  mulc1cncf 7222  ruclem13 7473  opnin 7821  fsumcnlem 7939  grpidinvlem3 8000  mulid 8084  ipasslem3 8436  hilid 8967  occllem6 9117  spanun 9405  5oalem3 9541  5oalem5 9543  mdslmd1lem2 10190
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 147  df-an 225
Copyright terms: Public domain