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  2032  eqsnm  3770  fnressn  5723  fressnfv  5724  eluniimadm  5787  genpassl  7554  genpassu  7555  1idprl  7620  1idpru  7621  axcaucvglemres  7929  negeq0  8242  muleqadd  8656  crap0  8946  addltmul  9186  fzrev  10116  modq0  10362  cjap0  10951  cjne0  10952  caucvgrelemrec  11023  lenegsq  11139  isumss  11434  fsumsplit  11450  sumsplitdc  11475  dvdsabseq  11888  pceu  12330  oddennn  12446  xpsfrnel  12823  metrest  14483  elabgf0  15007