Theorem bitr2d 188

Description: Deduction form of bitr2i 184. (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 187	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	3	bicomd 140	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitrrd  214  3bitr2rd  216  pm5.18dc  869  drex1  1771  elrnmpt1  4798  xpopth  6082  sbcopeq1a  6093  ltnnnq  7255  ltaddsub  8222  leaddsub  8224  posdif  8241  lesub1  8242  ltsub1  8244  lesub0  8265  possumd  8355  subap0  8429  ltdivmul  8658  ledivmul  8659  zlem1lt  9134  zltlem1  9135  negelrp  9504  fzrev2  9896  fz1sbc  9907  elfzp1b  9908  qtri3or  10051  sumsqeq0  10402  sqrtle  10840  sqrtlt  10841  absgt0ap  10903  iser3shft  11147  dvdssubr  11575  gcdn0gt0  11702  divgcdcoprmex  11819  lmbrf  12423  logge0b  13019  loggt0b  13020  logle1b  13021  loglt1b  13022