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  4975  xpopth  6328  sbcopeq1a  6339  ltnnnq  7618  ltaddsub  8591  leaddsub  8593  posdif  8610  lesub1  8611  ltsub1  8613  lesub0  8634  possumd  8724  subap0  8798  ltdivmul  9031  ledivmul  9032  zlem1lt  9511  zltlem1  9512  negelrp  9891  fzrev2  10289  fz1sbc  10300  elfzp1b  10301  qtri3or  10468  sumsqeq0  10848  sqrtle  11555  sqrtlt  11556  absgt0ap  11618  iser3shft  11865  dvdssubr  12358  gcdn0gt0  12507  divgcdcoprmex  12632  pcfac  12881  gsumfzval  13432  lmbrf  14897  logge0b  15572  loggt0b  15573  logle1b  15574  loglt1b  15575  lgsne0  15725  lgsprme0  15729