Theorem bitr3id 193

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

Hypotheses

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

Assertion

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

Proof of Theorem bitr3id

Step	Hyp	Ref	Expression
1		bitr3id.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	bicomi 131	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3id.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	syl5bb 191	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 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  885  19.16  1535  19.19  1645  cbvab  2264  necon1bbiidc  2370  rspc2gv  2805  elabgt  2829  sbceq1a  2922  sbcralt  2989  sbcrext  2990  sbccsbg  3036  sbccsb2g  3037  iunpw  4409  tfis  4505  xp11m  4985  ressn  5087  fnssresb  5243  fun11iun  5396  funimass4  5480  dffo4  5576  f1ompt  5579  fliftf  5708  resoprab2  5876  ralrnmpo  5893  rexrnmpo  5894  1stconst  6126  2ndconst  6127  dfsmo2  6192  smoiso  6207  brecop  6527  ixpsnf1o  6638  ac6sfi  6800  ismkvnex  7037  prarloclemn  7331  axcaucvglemres  7731  reapti  8365  indstr  9415  iccneg  9802  sqap0  10390  sqrt00  10844  minclpr  11040  fprodseq  11384  absefib  11513  efieq1re  11514  prmind2  11837  sincosq3sgn  12957  sincosq4sgn  12958  pw1nct  13371  iswomninnlem  13417