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  3742  fnressn  5682  fressnfv  5683  eluniimadm  5744  genpassl  7486  genpassu  7487  1idprl  7552  1idpru  7553  axcaucvglemres  7861  negeq0  8173  muleqadd  8586  crap0  8874  addltmul  9114  fzrev  10040  modq0  10285  cjap0  10871  cjne0  10872  caucvgrelemrec  10943  lenegsq  11059  isumss  11354  fsumsplit  11370  sumsplitdc  11395  dvdsabseq  11807  pceu  12249  oddennn  12347  metrest  13300  elabgf0  13812