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  1436  sbal2  2073  eqsnm  3838  fnressn  5840  fressnfv  5841  eluniimadm  5906  iftrueb01  7441  genpassl  7744  genpassu  7745  1idprl  7810  1idpru  7811  axcaucvglemres  8119  negeq0  8433  muleqadd  8848  crap0  9138  addltmul  9381  fzrev  10319  modq0  10592  cjap0  11469  cjne0  11470  caucvgrelemrec  11541  lenegsq  11657  isumss  11954  fsumsplit  11970  sumsplitdc  11995  dvdsabseq  12410  pceu  12870  oddennn  13015  xpsfrnel  13429  metrest  15233  elabgf0  16394