Theorem sylan2br 455

Description: A syllogism inference.

Hypotheses

Ref	Expression
sylan.1	|- ((ph /\ ps) -> ch)
sylan2br.2	|- (ps <-> th)

Assertion

Ref	Expression
sylan2br	|- ((ph /\ th) -> ch)

Proof of Theorem sylan2br

Step	Hyp	Ref	Expression
1		sylan.1	. 2 |- ((ph /\ ps) -> ch)
2		sylan2br.2	. . 3 |- (ps <-> th)
3	2	biimpr 152	. 2 |- (th -> ps)
4	1, 3	sylan2 453	1 |- ((ph /\ th) -> ch)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  syl2anbr 458  pm2.61ne 1636  nn0suc 3160  tfindsg2 3169  imainss 3469  xpexr2 3486  imadif 3580  fnop 3597  ssimaex 3774  tfrlem2 3918  tz7.48-2 3963  rankxplim3 4724  aceq5 4750  ac6lem 4764  zorn2lem7 4804  suppsr 5234  supsrlem6 5242  supre 5272  xrltnsymt 5562  xrsupsslem 6078  xrinfmsslem 6079  uzind3 6209  uzind3OLD 6211  bcval4t 6961  clm3 7079  climconst2 7095  cvgratlem3ALT 7249  cvgratlem3 7252  ef0lem 7310  elcls 7701  neiint 7716  neips 7724  cnconst 7777  bopcnlem2 7979  sqcn 8331  minveclem31 8571  hiidge0t 8959  normgt0tOLD 8988  hommvalt 9507  hfmmvalt 9510  eigorth 9758  nmcoplb 9953  nmophm 9956  nmbdfnlb 9973  nmcfnlb 9982  mdslmd1 10251  mdslmd3 10254  sumdmdlem2 10341  fiiu 10444

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