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  3833  fnressn  5832  fressnfv  5833  eluniimadm  5898  iftrueb01  7424  genpassl  7727  genpassu  7728  1idprl  7793  1idpru  7794  axcaucvglemres  8102  negeq0  8416  muleqadd  8831  crap0  9121  addltmul  9364  fzrev  10297  modq0  10568  cjap0  11439  cjne0  11440  caucvgrelemrec  11511  lenegsq  11627  isumss  11923  fsumsplit  11939  sumsplitdc  11964  dvdsabseq  12379  pceu  12839  oddennn  12984  xpsfrnel  13398  metrest  15201  elabgf0  16250