Theorem syl5bbr 250

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  3bitr3g  278  biass  348  19.16  1860  19.19  1862  sbco2  2086  cbvab  2472  necon1bbid  2571  necon4abid  2581  elabgt  2983  sbceq1a  3057  sbcralt  3119  sbccsbg  3165  sbccsb2g  3166  opkelimagekg  4272  vfin1cltv  4548  phialllem1  4617  phiall  4619  xp11  5057  nfunv  5139  fnssresb  5196  fun11iun  5306  dffo4  5424  elunirn  5471  isomin  5497  resoprab2  5583  nchoicelem11  6300