Theorem bitr3id 194

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 132	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3id.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	bitrid 192	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3bitr3g  222  imbibi  252  ianordc  900  19.16  1566  19.19  1677  cbvab  2313  necon1bbiidc  2421  rspc2gv  2868  elabgt  2893  sbceq1a  2987  sbcralt  3054  sbcrext  3055  sbccsbg  3101  sbccsb2g  3102  iunpw  4498  tfis  4600  xp11m  5085  ressn  5187  fnssresb  5347  fun11iun  5501  funimass4  5587  dffo4  5685  f1ompt  5688  fliftf  5821  resoprab2  5994  ralrnmpo  6012  rexrnmpo  6013  1stconst  6247  2ndconst  6248  dfsmo2  6313  smoiso  6328  brecop  6652  ixpsnf1o  6763  ac6sfi  6927  ismkvnex  7184  nninfwlporlemd  7201  prarloclemn  7529  axcaucvglemres  7929  reapti  8567  indstr  9625  iccneg  10021  sqap0  10621  sqrt00  11084  minclpr  11280  fprodseq  11626  absefib  11813  efieq1re  11814  prmind2  12155  gsumval2  12875  eqgval  13179  sincosq3sgn  14726  sincosq4sgn  14727  lgsdinn0  14927  pw1nct  15231  iswomninnlem  15276