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  2039  eqsnm  3786  fnressn  5751  fressnfv  5752  eluniimadm  5815  genpassl  7610  genpassu  7611  1idprl  7676  1idpru  7677  axcaucvglemres  7985  negeq0  8299  muleqadd  8714  crap0  9004  addltmul  9247  fzrev  10178  modq0  10440  cjap0  11091  cjne0  11092  caucvgrelemrec  11163  lenegsq  11279  isumss  11575  fsumsplit  11591  sumsplitdc  11616  dvdsabseq  12031  pceu  12491  oddennn  12636  xpsfrnel  13048  metrest  14828  elabgf0  15509