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  888  drex1  1844  elrnmpt1  4978  xpopth  6331  sbcopeq1a  6342  ltnnnq  7626  ltaddsub  8599  leaddsub  8601  posdif  8618  lesub1  8619  ltsub1  8621  lesub0  8642  possumd  8732  subap0  8806  ltdivmul  9039  ledivmul  9040  zlem1lt  9519  zltlem1  9520  negelrp  9900  fzrev2  10298  fz1sbc  10309  elfzp1b  10310  qtri3or  10477  sumsqeq0  10857  sqrtle  11568  sqrtlt  11569  absgt0ap  11631  iser3shft  11878  dvdssubr  12371  gcdn0gt0  12520  divgcdcoprmex  12645  pcfac  12894  gsumfzval  13445  lmbrf  14910  logge0b  15585  loggt0b  15586  logle1b  15587  loglt1b  15588  lgsne0  15738  lgsprme0  15742