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  798  19.16  1444  19.19  1553  cbvab  2157  necon1bbiidc  2260  elabgt  2678  sbceq1a  2767  sbcralt  2828  sbcrext  2829  sbccsbg  2872  sbccsb2g  2873  iunpw  4177  tfis  4249  xp11m  4702  ressn  4801  fnssresb  4954  fun11iun  5090  funimass4  5167  dffo4  5258  f1ompt  5263  fliftf  5382  resoprab2  5540  ralrnmpt2  5557  rexrnmpt2  5558  1stconst  5784  2ndconst  5785  dfsmo2  5843  smoiso  5858  brecop  6132  prarloclemn  6482  reapti  7363  indstr  8312  iccneg  8627