Theorem bitr2d 189

Description: Deduction form of bitr2i 185. (Contributed by NM, 9-Jun-2004.)

Hypotheses

Ref	Expression
bitr2d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitr2d.2	⊢ (𝜑 → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
bitr2d	⊢ (𝜑 → (𝜃 ↔ 𝜓))

Proof of Theorem bitr2d

Step	Hyp	Ref	Expression
1		bitr2d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitr2d.2	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
3	1, 2	bitrd 188	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	3	bicomd 141	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:  3bitrrd  215  3bitr2rd  217  pm5.18dc  895  drex1  1851  elrnmpt1  5033  xpopth  6410  sbcopeq1a  6421  ltnnnq  7790  ltaddsub  8764  leaddsub  8766  posdif  8783  lesub1  8784  ltsub1  8786  lesub0  8807  possumd  8898  subap0  8972  ltdivmul  9207  ledivmul  9208  zlem1lt  9703  zltlem1  9704  negelrp  10090  fzrev2  10494  fz1sbc  10505  elfzp1b  10506  qtri3or  10677  sumsqeq0  11057  sqrtle  11804  sqrtlt  11805  absgt0ap  11867  iser3shft  12114  dvdssubr  12608  gcdn0gt0  12757  divgcdcoprmex  12882  pcfac  13131  gzsumfzval  13713  lmbrf  15318  reaplog  15972  logge0b  15995  loggt0b  15996  logle1b  15997  loglt1b  15998  lgsne0  16169  lgsprme0  16173