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  5035  xpopth  6414  sbcopeq1a  6425  ltnnnq  7796  ltaddsub  8771  leaddsub  8773  posdif  8790  lesub1  8791  ltsub1  8793  lesub0  8814  possumd  8905  subap0  8979  ltdivmul  9214  ledivmul  9215  zlem1lt  9710  zltlem1  9711  negelrp  10104  fzrev2  10508  fz1sbc  10519  elfzp1b  10520  qtri3or  10691  sumsqeq0  11075  sqrtle  11823  sqrtlt  11824  absgt0ap  11887  iser3shft  12136  dvdssubr  12630  gcdn0gt0  12779  divgcdcoprmex  12904  pcfac  13157  gzsumfzval  13769  lmbrf  15458  sineq0re  16093  reaplog  16114  logge0b  16137  loggt0b  16138  logle1b  16139  loglt1b  16140  bposlem7  16334  lgsne0  16379  lgsprme0  16383