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  1434  sbal2  2071  eqsnm  3833  fnressn  5829  fressnfv  5830  eluniimadm  5895  iftrueb01  7416  genpassl  7719  genpassu  7720  1idprl  7785  1idpru  7786  axcaucvglemres  8094  negeq0  8408  muleqadd  8823  crap0  9113  addltmul  9356  fzrev  10288  modq0  10559  cjap0  11426  cjne0  11427  caucvgrelemrec  11498  lenegsq  11614  isumss  11910  fsumsplit  11926  sumsplitdc  11951  dvdsabseq  12366  pceu  12826  oddennn  12971  xpsfrnel  13385  metrest  15188  elabgf0  16165