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 1625  nn0suc 3144  tfindsg2 3153  imainss 3449  xpexr2 3466  imadif 3560  fnop 3577  ssimaex 3753  tfrlem2 3897  tz7.48-2 3942  rankxplim3 4686  aceq5 4712  ac6lem 4726  zorn2lem7 4766  suppsr 5194  supsrlem6 5202  supre 5232  xrltnsymt 5523  xrsupsslem 6023  xrinfmsslem 6024  uzind3 6155  uzind3OLD 6157  bcval4t 6899  clm3 7017  climconst2 7032  cvgratlem3ALT 7184  cvgratlem3 7187  ef0lem 7252  elcls 7646  neiint 7660  neips 7668  cnconst 7719  bopcnlem2 7916  sqcn 8270  minveclem31 8506  hiidge0t 8885  normgt0tOLD 8914  hommvalt 9429  hfmmvalt 9432  eigorth 9680  nmcoplb 9873  nmophm 9876  nmbdfnlb 9893  nmcfnlb 9902  mdslmd1 10164  mdslmd3 10167  sumdmdlem2 10253  fiiu 10350

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