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  2074  eqsnm  3858  fnressn  5869  fressnfv  5870  eluniimadm  5937  iftrueb01  7532  genpassl  7835  genpassu  7836  1idprl  7901  1idpru  7902  axcaucvglemres  8210  negeq0  8523  muleqadd  8938  crap0  9228  addltmul  9471  fzrev  10414  modq0  10687  cjap0  11585  cjne0  11586  caucvgrelemrec  11657  lenegsq  11773  isumss  12070  fsumsplit  12086  sumsplitdc  12111  dvdsabseq  12526  pceu  12986  oddennn  13132  xpsfrnel  13546  metrest  15358  elabgf0  16536