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  1412  sbal2  2049  eqsnm  3798  fnressn  5777  fressnfv  5778  eluniimadm  5841  genpassl  7644  genpassu  7645  1idprl  7710  1idpru  7711  axcaucvglemres  8019  negeq0  8333  muleqadd  8748  crap0  9038  addltmul  9281  fzrev  10213  modq0  10481  cjap0  11262  cjne0  11263  caucvgrelemrec  11334  lenegsq  11450  isumss  11746  fsumsplit  11762  sumsplitdc  11787  dvdsabseq  12202  pceu  12662  oddennn  12807  xpsfrnel  13220  metrest  15022  elabgf0  15787