Theorem bitr3di 194

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 131	. 2 ⊢ (𝜃 ↔ 𝜓)
3		bitr3di.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	bitr2id 192	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  xordc  1382  sbal2  2008  eqsnm  3734  fnressn  5670  fressnfv  5671  eluniimadm  5732  genpassl  7461  genpassu  7462  1idprl  7527  1idpru  7528  axcaucvglemres  7836  negeq0  8148  muleqadd  8561  crap0  8849  addltmul  9089  fzrev  10015  modq0  10260  cjap0  10845  cjne0  10846  caucvgrelemrec  10917  lenegsq  11033  isumss  11328  fsumsplit  11344  sumsplitdc  11369  dvdsabseq  11781  pceu  12223  oddennn  12321  metrest  13106  elabgf0  13618