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

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:  3bitrrd  215  3bitr2rd  217  pm5.18dc  884  drex1  1809  elrnmpt1  4913  xpopth  6229  sbcopeq1a  6240  ltnnnq  7483  ltaddsub  8455  leaddsub  8457  posdif  8474  lesub1  8475  ltsub1  8477  lesub0  8498  possumd  8588  subap0  8662  ltdivmul  8895  ledivmul  8896  zlem1lt  9373  zltlem1  9374  negelrp  9753  fzrev2  10151  fz1sbc  10162  elfzp1b  10163  qtri3or  10310  sumsqeq0  10689  sqrtle  11180  sqrtlt  11181  absgt0ap  11243  iser3shft  11489  dvdssubr  11982  gcdn0gt0  12115  divgcdcoprmex  12240  pcfac  12488  gsumfzval  12974  lmbrf  14383  logge0b  15025  loggt0b  15026  logle1b  15027  loglt1b  15028  lgsne0  15154  lgsprme0  15158