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  891  drex1  1847  elrnmpt1  5013  xpopth  6383  sbcopeq1a  6394  ltnnnq  7754  ltaddsub  8728  leaddsub  8730  posdif  8747  lesub1  8748  ltsub1  8750  lesub0  8771  possumd  8861  subap0  8935  ltdivmul  9170  ledivmul  9171  zlem1lt  9654  zltlem1  9655  negelrp  10041  fzrev2  10444  fz1sbc  10455  elfzp1b  10456  qtri3or  10627  sumsqeq0  11007  sqrtle  11749  sqrtlt  11750  absgt0ap  11812  iser3shft  12059  dvdssubr  12553  gcdn0gt0  12702  divgcdcoprmex  12827  pcfac  13076  gsumfzval  13657  lmbrf  15209  logge0b  15884  loggt0b  15885  logle1b  15886  loglt1b  15887  lgsne0  16040  lgsprme0  16044