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  5010  xpopth  6372  sbcopeq1a  6383  ltnnnq  7743  ltaddsub  8715  leaddsub  8717  posdif  8734  lesub1  8735  ltsub1  8737  lesub0  8758  possumd  8848  subap0  8922  ltdivmul  9155  ledivmul  9156  zlem1lt  9639  zltlem1  9640  negelrp  10026  fzrev2  10426  fz1sbc  10437  elfzp1b  10438  qtri3or  10607  sumsqeq0  10987  sqrtle  11729  sqrtlt  11730  absgt0ap  11792  iser3shft  12039  dvdssubr  12533  gcdn0gt0  12682  divgcdcoprmex  12807  pcfac  13056  gsumfzval  13625  lmbrf  15129  logge0b  15804  loggt0b  15805  logle1b  15806  loglt1b  15807  lgsne0  15960  lgsprme0  15964