Theorem syl5bbr 193

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 131	. 2 ⊢ (𝜑 ↔ 𝜓)
3		syl5bbr.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	syl5bb 191	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 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  838  19.16  1493  19.19  1602  cbvab  2211  necon1bbiidc  2317  rspc2gv  2734  elabgt  2758  sbceq1a  2850  sbcralt  2916  sbcrext  2917  sbccsbg  2960  sbccsb2g  2961  iunpw  4315  tfis  4411  xp11m  4882  ressn  4984  fnssresb  5139  fun11iun  5287  funimass4  5368  dffo4  5461  f1ompt  5464  fliftf  5592  resoprab2  5756  ralrnmpt2  5773  rexrnmpt2  5774  1stconst  6000  2ndconst  6001  dfsmo2  6066  smoiso  6081  brecop  6396  ixpsnf1o  6507  ac6sfi  6668  prarloclemn  7119  axcaucvglemres  7495  reapti  8117  indstr  9142  iccneg  9467  sqap0  10082  sqrt00  10534  absefib  11121  efieq1re  11122  prmind2  11441