Theorem bitr3di 194

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 131	. 2 ⊢ (𝜃 ↔ 𝜓)
3		bitr3di.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	bitr2id 192	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  xordc  1387  sbal2  2013  eqsnm  3740  fnressn  5679  fressnfv  5680  eluniimadm  5741  genpassl  7473  genpassu  7474  1idprl  7539  1idpru  7540  axcaucvglemres  7848  negeq0  8160  muleqadd  8573  crap0  8861  addltmul  9101  fzrev  10027  modq0  10272  cjap0  10858  cjne0  10859  caucvgrelemrec  10930  lenegsq  11046  isumss  11341  fsumsplit  11357  sumsplitdc  11382  dvdsabseq  11794  pceu  12236  oddennn  12334  metrest  13221  elabgf0  13733