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  7797  ltaddsub  8772  leaddsub  8774  posdif  8791  lesub1  8792  ltsub1  8794  lesub0  8815  possumd  8906  subap0  8980  ltdivmul  9215  ledivmul  9216  zlem1lt  9713  zltlem1  9714  negelrp  10106  fzrev2  10510  fz1sbc  10521  elfzp1b  10522  qtri3or  10693  sumsqeq0  11077  sqrtle  11825  sqrtlt  11826  absgt0ap  11889  iser3shft  12138  dvdssubr  12632  gcdn0gt0  12781  divgcdcoprmex  12906  pcfac  13159  gzsumfzval  13771  lmbrf  15453  sineq0re  16088  reaplog  16109  logge0b  16132  loggt0b  16133  logle1b  16134  loglt1b  16135  bposlem7  16329  lgsne0  16374  lgsprme0  16378