Theorem syl5bbr 193

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl5bbr.1	|- ( ps <-> ph )
syl5bbr.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
syl5bbr	|- ( ch -> ( ph <-> th ) )

Proof of Theorem syl5bbr

Step	Hyp	Ref	Expression
1		syl5bbr.1	. . 3 |- ( ps <-> ph )
2	1	bicomi 131	. 2 |- ( ph <-> ps )
3		syl5bbr.2	. 2 |- ( ch -> ( ps <-> th ) )
4	2, 3	syl5bb 191	1 |- ( ch -> ( ph <-> th ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitr3g  221  ianordc  865  19.16  1515  19.19  1625  cbvab  2235  necon1bbiidc  2341  rspc2gv  2769  elabgt  2793  sbceq1a  2885  sbcralt  2951  sbcrext  2952  sbccsbg  2995  sbccsb2g  2996  iunpw  4359  tfis  4455  xp11m  4933  ressn  5035  fnssresb  5191  fun11iun  5342  funimass4  5424  dffo4  5520  f1ompt  5523  fliftf  5652  resoprab2  5820  ralrnmpo  5837  rexrnmpo  5838  1stconst  6070  2ndconst  6071  dfsmo2  6136  smoiso  6151  brecop  6471  ixpsnf1o  6582  ac6sfi  6743  prarloclemn  7249  axcaucvglemres  7628  reapti  8253  indstr  9284  iccneg  9659  sqap0  10246  sqrt00  10698  minclpr  10894  absefib  11321  efieq1re  11322  prmind2  11641