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  1441  sbal2  2080  eqsnm  3878  fnressn  5895  fressnfv  5896  eluniimadm  5965  iftrueb01  7576  genpassl  7885  genpassu  7886  1idprl  7951  1idpru  7952  axcaucvglemres  8260  negeq0  8574  addeq0  8697  msqap0  8990  muleqadd  8992  crap0  9282  addltmul  9525  fzrev  10474  modq0  10749  cjap0  11656  cjne0  11657  caucvgrelemrec  11728  lenegsq  11844  isumss  12141  fsumsplit  12157  sumsplitdc  12182  dvdsabseq  12597  pceu  13057  oddennn  13266  xpsfrnel  13648  metrest  15590  elabgf0  16788