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-mp 5  ax-1 6  ax-2 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  884  19.16  1534  19.19  1644  cbvab  2263  necon1bbiidc  2369  rspc2gv  2801  elabgt  2825  sbceq1a  2918  sbcralt  2985  sbcrext  2986  sbccsbg  3031  sbccsb2g  3032  iunpw  4401  tfis  4497  xp11m  4977  ressn  5079  fnssresb  5235  fun11iun  5388  funimass4  5472  dffo4  5568  f1ompt  5571  fliftf  5700  resoprab2  5868  ralrnmpo  5885  rexrnmpo  5886  1stconst  6118  2ndconst  6119  dfsmo2  6184  smoiso  6199  brecop  6519  ixpsnf1o  6630  ac6sfi  6792  ismkvnex  7029  prarloclemn  7307  axcaucvglemres  7707  reapti  8341  indstr  9388  iccneg  9772  sqap0  10359  sqrt00  10812  minclpr  11008  absefib  11477  efieq1re  11478  prmind2  11801  sincosq3sgn  12909  sincosq4sgn  12910