Theorem syl5bbr 192

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

Hypotheses

Ref	Expression
syl5bbr.1	⊢ (𝜓 ↔ 𝜑)
syl5bbr.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
syl5bbr	⊢ (𝜒 → (𝜑 ↔ 𝜃))

Proof of Theorem syl5bbr

Step	Hyp	Ref	Expression
1		syl5bbr.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	bicomi 130	. 2 ⊢ (𝜑 ↔ 𝜓)
3		syl5bbr.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	syl5bb 190	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3bitr3g  220  ianordc  832  19.16  1487  19.19  1596  cbvab  2201  necon1bbiidc  2306  rspc2gv  2712  elabgt  2735  sbceq1a  2824  sbcralt  2890  sbcrext  2891  sbccsbg  2934  sbccsb2g  2935  iunpw  4229  tfis  4324  xp11m  4779  ressn  4878  fnssresb  5031  fun11iun  5167  funimass4  5245  dffo4  5336  f1ompt  5341  fliftf  5459  resoprab2  5618  ralrnmpt2  5635  rexrnmpt2  5636  1stconst  5862  2ndconst  5863  dfsmo2  5925  smoiso  5940  brecop  6219  ac6sfi  6379  prarloclemn  6689  axcaucvglemres  7065  reapti  7679  indstr  8681  iccneg  9011  sqap0  9542  sqrt00  9926  prmind2  10502