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  5904  fressnfv  5905  eluniimadm  5974  iftrueb01  7589  genpassl  7898  genpassu  7899  1idprl  7964  1idpru  7965  axcaucvglemres  8273  negeq0  8588  addeq0  8711  msqap0  9005  muleqadd  9007  crap0  9297  addltmul  9554  fzrev  10509  modq0  10788  cjap0  11696  cjne0  11697  caucvgrelemrec  11768  lenegsq  11885  isumss  12184  fsumsplit  12200  sumsplitdc  12225  dvdsabseq  12640  pceu  13104  oddennn  13342  xpsfrnel  13725  resscntz  14167  metrest  15744  elabgf0  17022