Theorem sylan2br 453

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 451	1 |- ((ph /\ th) -> ch)

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

This theorem is referenced by:  syl2anbr 456  pm2.61ne 1633  nn0suc 3154  tfindsg2 3163  imainss 3463  xpexr2 3480  imadif 3574  fnop 3591  ssimaex 3768  tfrlem2 3912  tz7.48-2 3957  rankxplim3 4714  aceq5 4740  ac6lem 4754  zorn2lem7 4794  suppsr 5222  supsrlem6 5230  supre 5260  xrltnsymt 5550  xrsupsslem 6076  xrinfmsslem 6077  uzind3 6207  uzind3OLD 6209  bcval4t 6961  clm3 7079  climconst2 7095  cvgratlem3ALT 7249  cvgratlem3 7252  ef0lem 7310  elcls 7704  neiint 7719  neips 7727  cnconst 7780  bopcnlem2 7982  sqcn 8335  minveclem31 8575  hiidge0t 8964  normgt0tOLD 8993  hommvalt 9512  hfmmvalt 9515  eigorth 9763  nmcoplb 9958  nmophm 9961  nmbdfnlb 9978  nmcfnlb 9987  mdslmd1 10256  mdslmd3 10259  sumdmdlem2 10346  fiiu 10453  fiiuOLD 10454

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