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  883  drex1  1798  elrnmpt1  4880  xpopth  6179  sbcopeq1a  6190  ltnnnq  7424  ltaddsub  8395  leaddsub  8397  posdif  8414  lesub1  8415  ltsub1  8417  lesub0  8438  possumd  8528  subap0  8602  ltdivmul  8835  ledivmul  8836  zlem1lt  9311  zltlem1  9312  negelrp  9689  fzrev2  10087  fz1sbc  10098  elfzp1b  10099  qtri3or  10245  sumsqeq0  10601  sqrtle  11047  sqrtlt  11048  absgt0ap  11110  iser3shft  11356  dvdssubr  11848  gcdn0gt0  11981  divgcdcoprmex  12104  pcfac  12350  lmbrf  13800  logge0b  14396  loggt0b  14397  logle1b  14398  loglt1b  14399  lgsne0  14524  lgsprme0  14528