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  2036  eqsnm  3781  fnressn  5744  fressnfv  5745  eluniimadm  5808  genpassl  7584  genpassu  7585  1idprl  7650  1idpru  7651  axcaucvglemres  7959  negeq0  8273  muleqadd  8687  crap0  8977  addltmul  9219  fzrev  10150  modq0  10400  cjap0  11051  cjne0  11052  caucvgrelemrec  11123  lenegsq  11239  isumss  11534  fsumsplit  11550  sumsplitdc  11575  dvdsabseq  11989  pceu  12433  oddennn  12549  xpsfrnel  12927  metrest  14674  elabgf0  15269