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  887  drex1  1824  elrnmpt1  4951  xpopth  6292  sbcopeq1a  6303  ltnnnq  7578  ltaddsub  8551  leaddsub  8553  posdif  8570  lesub1  8571  ltsub1  8573  lesub0  8594  possumd  8684  subap0  8758  ltdivmul  8991  ledivmul  8992  zlem1lt  9471  zltlem1  9472  negelrp  9851  fzrev2  10249  fz1sbc  10260  elfzp1b  10261  qtri3or  10427  sumsqeq0  10807  sqrtle  11513  sqrtlt  11514  absgt0ap  11576  iser3shft  11823  dvdssubr  12316  gcdn0gt0  12465  divgcdcoprmex  12590  pcfac  12839  gsumfzval  13390  lmbrf  14854  logge0b  15529  loggt0b  15530  logle1b  15531  loglt1b  15532  lgsne0  15682  lgsprme0  15686