Theorem syl5bbr 183

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 123	. 2 |- ( ph <-> ps )
3		syl5bbr.2	. 2 |- ( ch -> ( ps <-> th ) )
4	2, 3	syl5bb 181	1 |- ( ch -> ( ph <-> th ) )

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3bitr3g  211  ianordc  799  19.16  1447  19.19  1556  cbvab  2160  necon1bbiidc  2266  elabgt  2684  sbceq1a  2773  sbcralt  2834  sbcrext  2835  sbccsbg  2878  sbccsb2g  2879  iunpw  4211  tfis  4306  xp11m  4759  ressn  4858  fnssresb  5011  fun11iun  5147  funimass4  5224  dffo4  5315  f1ompt  5320  fliftf  5439  resoprab2  5598  ralrnmpt2  5615  rexrnmpt2  5616  1stconst  5842  2ndconst  5843  dfsmo2  5902  smoiso  5917  brecop  6196  ac6sfi  6352  prarloclemn  6595  axcaucvglemres  6971  reapti  7568  indstr  8534  iccneg  8855  sqap0  9294  sqrt00  9612