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  906  19.16  1603  19.19  1714  cbvab  2355  necon1bbiidc  2463  rspc2gv  2922  elabgt  2947  sbceq1a  3041  sbcralt  3108  sbcrext  3109  sbccsbg  3156  sbccsb2g  3157  iunpw  4577  tfis  4681  reldmm  4950  xp11m  5175  ressn  5277  fnssresb  5444  fun11iun  5604  funimass4  5696  dffo4  5795  f1ompt  5798  fliftf  5940  resoprab2  6118  ralrnmpo  6136  rexrnmpo  6137  1stconst  6386  2ndconst  6387  dfsmo2  6453  smoiso  6468  brecop  6794  ixpsnf1o  6905  ac6sfi  7087  ismkvnex  7354  nninfwlporlemd  7371  prarloclemn  7719  axcaucvglemres  8119  reapti  8759  indstr  9827  iccneg  10224  sqap0  10869  wrdmap  11146  wrdind  11304  sqrt00  11602  minclpr  11799  fprodseq  12146  absefib  12334  efieq1re  12335  prmind2  12694  gsumval2  13482  eqgval  13812  isnzr2  14201  sincosq3sgn  15555  sincosq4sgn  15556  fsumdvdsmul  15718  lgsdinn0  15780  pw1nct  16625  iswomninnlem  16674