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  904  19.16  1601  19.19  1712  cbvab  2353  necon1bbiidc  2461  rspc2gv  2920  elabgt  2945  sbceq1a  3039  sbcralt  3106  sbcrext  3107  sbccsbg  3154  sbccsb2g  3155  iunpw  4575  tfis  4679  reldmm  4948  xp11m  5173  ressn  5275  fnssresb  5441  fun11iun  5601  funimass4  5692  dffo4  5791  f1ompt  5794  fliftf  5935  resoprab2  6113  ralrnmpo  6131  rexrnmpo  6132  1stconst  6381  2ndconst  6382  dfsmo2  6448  smoiso  6463  brecop  6789  ixpsnf1o  6900  ac6sfi  7082  ismkvnex  7348  nninfwlporlemd  7365  prarloclemn  7712  axcaucvglemres  8112  reapti  8752  indstr  9820  iccneg  10217  sqap0  10861  wrdmap  11138  wrdind  11296  sqrt00  11594  minclpr  11791  fprodseq  12137  absefib  12325  efieq1re  12326  prmind2  12685  gsumval2  13473  eqgval  13803  isnzr2  14191  sincosq3sgn  15545  sincosq4sgn  15546  fsumdvdsmul  15708  lgsdinn0  15770  pw1nct  16554  iswomninnlem  16603