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 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  xordc  1441  sbal2  2080  eqsnm  3880  fnressn  5901  fressnfv  5902  eluniimadm  5971  iftrueb01  7582  genpassl  7891  genpassu  7892  1idprl  7957  1idpru  7958  axcaucvglemres  8266  negeq0  8580  addeq0  8703  msqap0  8997  muleqadd  8999  crap0  9289  addltmul  9544  fzrev  10493  modq0  10768  cjap0  11675  cjne0  11676  caucvgrelemrec  11747  lenegsq  11863  isumss  12160  fsumsplit  12176  sumsplitdc  12201  dvdsabseq  12616  pceu  13076  oddennn  13285  xpsfrnel  13667  metrest  15609  elabgf0  16817