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  907  19.16  1604  19.19  1714  cbvab  2358  necon1bbiidc  2473  rspc2gv  2932  elabgt  2957  sbceq1a  3051  sbcralt  3118  sbcrext  3119  sbccsbg  3166  sbccsb2g  3167  iunpw  4600  tfis  4704  reldmm  4974  xp11m  5200  ressn  5302  fnssresb  5469  fun11iun  5634  funimass4  5726  dffo4  5824  f1ompt  5827  fliftf  5971  resoprab2  6149  ralrnmpo  6167  rexrnmpo  6168  1stconst  6416  2ndconst  6417  dfsmo2  6517  smoiso  6532  brecop  6858  ixpsnf1o  6970  ac6sfi  7154  ismkvnex  7445  nninfwlporlemd  7462  prarloclemn  7810  axcaucvglemres  8210  reapti  8849  indstr  9921  iccneg  10318  sqap0  10964  wrdmap  11249  wrdind  11407  sqrt00  11718  minclpr  11915  fprodseq  12262  absefib  12450  efieq1re  12451  prmind2  12810  gsumval2  13599  eqgval  13929  isnzr2  14318  sincosq3sgn  15680  sincosq4sgn  15681  fsumdvdsmul  15846  lgsdinn0  15908  pw1nct  16764  iswomninnlem  16821