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  5007  xpopth  6369  sbcopeq1a  6380  ltnnnq  7734  ltaddsub  8706  leaddsub  8708  posdif  8725  lesub1  8726  ltsub1  8728  lesub0  8749  possumd  8839  subap0  8913  ltdivmul  9146  ledivmul  9147  zlem1lt  9630  zltlem1  9631  negelrp  10016  fzrev2  10415  fz1sbc  10426  elfzp1b  10427  qtri3or  10596  sumsqeq0  10976  sqrtle  11714  sqrtlt  11715  absgt0ap  11777  iser3shft  12024  dvdssubr  12518  gcdn0gt0  12667  divgcdcoprmex  12792  pcfac  13041  gsumfzval  13593  lmbrf  15067  logge0b  15742  loggt0b  15743  logle1b  15744  loglt1b  15745  lgsne0  15898  lgsprme0  15902