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  885  drex1  1822  elrnmpt1  4934  xpopth  6269  sbcopeq1a  6280  ltnnnq  7543  ltaddsub  8516  leaddsub  8518  posdif  8535  lesub1  8536  ltsub1  8538  lesub0  8559  possumd  8649  subap0  8723  ltdivmul  8956  ledivmul  8957  zlem1lt  9436  zltlem1  9437  negelrp  9816  fzrev2  10214  fz1sbc  10225  elfzp1b  10226  qtri3or  10390  sumsqeq0  10770  sqrtle  11391  sqrtlt  11392  absgt0ap  11454  iser3shft  11701  dvdssubr  12194  gcdn0gt0  12343  divgcdcoprmex  12468  pcfac  12717  gsumfzval  13267  lmbrf  14731  logge0b  15406  loggt0b  15407  logle1b  15408  loglt1b  15409  lgsne0  15559  lgsprme0  15563