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  1437  sbal2  2076  eqsnm  3861  fnressn  5872  fressnfv  5873  eluniimadm  5940  iftrueb01  7535  genpassl  7844  genpassu  7845  1idprl  7910  1idpru  7911  axcaucvglemres  8219  negeq0  8532  muleqadd  8947  crap0  9237  addltmul  9480  fzrev  10425  modq0  10698  cjap0  11600  cjne0  11601  caucvgrelemrec  11672  lenegsq  11788  isumss  12085  fsumsplit  12101  sumsplitdc  12126  dvdsabseq  12541  pceu  13001  oddennn  13164  xpsfrnel  13578  metrest  15420  elabgf0  16598