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  3836  fnressn  5835  fressnfv  5836  eluniimadm  5901  iftrueb01  7434  genpassl  7737  genpassu  7738  1idprl  7803  1idpru  7804  axcaucvglemres  8112  negeq0  8426  muleqadd  8841  crap0  9131  addltmul  9374  fzrev  10312  modq0  10584  cjap0  11461  cjne0  11462  caucvgrelemrec  11533  lenegsq  11649  isumss  11945  fsumsplit  11961  sumsplitdc  11986  dvdsabseq  12401  pceu  12861  oddennn  13006  xpsfrnel  13420  metrest  15223  elabgf0  16323