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  4495  tfis  4597  xp11m  5082  ressn  5184  fnssresb  5344  fun11iun  5498  funimass4  5583  dffo4  5681  f1ompt  5684  fliftf  5817  resoprab2  5989  ralrnmpo  6007  rexrnmpo  6008  1stconst  6241  2ndconst  6242  dfsmo2  6307  smoiso  6322  brecop  6644  ixpsnf1o  6755  ac6sfi  6917  ismkvnex  7173  nninfwlporlemd  7190  prarloclemn  7518  axcaucvglemres  7918  reapti  8556  indstr  9613  iccneg  10009  sqap0  10607  sqrt00  11069  minclpr  11265  fprodseq  11611  absefib  11798  efieq1re  11799  prmind2  12140  eqgval  13135  sincosq3sgn  14653  sincosq4sgn  14654  lgsdinn0  14853  pw1nct  15157  iswomninnlem  15202