Theorem bitr3di 195

Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)

Hypotheses

Ref	Expression
bitr3di.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitr3di.2	⊢ (𝜓 ↔ 𝜃)

Assertion

Ref	Expression
bitr3di	⊢ (𝜑 → (𝜒 ↔ 𝜃))

Proof of Theorem bitr3di

Step	Hyp	Ref	Expression
1		bitr3di.2	. . 3 ⊢ (𝜓 ↔ 𝜃)
2	1	bicomi 132	. 2 ⊢ (𝜃 ↔ 𝜓)
3		bitr3di.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	bitr2id 193	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:  xordc  1437  sbal2  2076  eqsnm  3864  fnressn  5875  fressnfv  5876  eluniimadm  5944  iftrueb01  7546  genpassl  7855  genpassu  7856  1idprl  7921  1idpru  7922  axcaucvglemres  8230  negeq0  8544  addeq0  8667  msqap0  8960  muleqadd  8962  crap0  9252  addltmul  9495  fzrev  10443  modq0  10718  cjap0  11620  cjne0  11621  caucvgrelemrec  11692  lenegsq  11808  isumss  12105  fsumsplit  12121  sumsplitdc  12146  dvdsabseq  12561  pceu  13021  oddennn  13230  xpsfrnel  13611  metrest  15500  elabgf0  16688