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  1403  sbal2  2036  eqsnm  3782  fnressn  5745  fressnfv  5746  eluniimadm  5809  genpassl  7586  genpassu  7587  1idprl  7652  1idpru  7653  axcaucvglemres  7961  negeq0  8275  muleqadd  8689  crap0  8979  addltmul  9222  fzrev  10153  modq0  10403  cjap0  11054  cjne0  11055  caucvgrelemrec  11126  lenegsq  11242  isumss  11537  fsumsplit  11553  sumsplitdc  11578  dvdsabseq  11992  pceu  12436  oddennn  12552  xpsfrnel  12930  metrest  14685  elabgf0  15339