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  1436  sbal2  2072  eqsnm  3839  fnressn  5843  fressnfv  5844  eluniimadm  5911  iftrueb01  7446  genpassl  7749  genpassu  7750  1idprl  7815  1idpru  7816  axcaucvglemres  8124  negeq0  8438  muleqadd  8853  crap0  9143  addltmul  9386  fzrev  10324  modq0  10597  cjap0  11490  cjne0  11491  caucvgrelemrec  11562  lenegsq  11678  isumss  11975  fsumsplit  11991  sumsplitdc  12016  dvdsabseq  12431  pceu  12891  oddennn  13036  xpsfrnel  13450  metrest  15259  elabgf0  16434