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-1 5  ax-2 6  ax-mp 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  821  drex1  1737  elrnmpt1  4728  xpopth  6004  sbcopeq1a  6015  ltnnnq  7132  ltaddsub  8065  leaddsub  8067  posdif  8084  lesub1  8085  ltsub1  8087  lesub0  8108  possumd  8197  subap0  8270  ltdivmul  8492  ledivmul  8493  zlem1lt  8962  zltlem1  8963  fzrev2  9706  fz1sbc  9717  elfzp1b  9718  qtri3or  9861  sumsqeq0  10212  sqrtle  10648  sqrtlt  10649  absgt0ap  10711  iser3shft  10954  dvdssubr  11334  gcdn0gt0  11461  divgcdcoprmex  11576  lmbrf  12165