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  895  drex1  1851  elrnmpt1  5031  xpopth  6404  sbcopeq1a  6415  ltnnnq  7784  ltaddsub  8758  leaddsub  8760  posdif  8777  lesub1  8778  ltsub1  8780  lesub0  8801  possumd  8891  subap0  8965  ltdivmul  9200  ledivmul  9201  zlem1lt  9684  zltlem1  9685  negelrp  10071  fzrev2  10475  fz1sbc  10486  elfzp1b  10487  qtri3or  10658  sumsqeq0  11038  sqrtle  11785  sqrtlt  11786  absgt0ap  11848  iser3shft  12095  dvdssubr  12589  gcdn0gt0  12738  divgcdcoprmex  12863  pcfac  13112  gzsumfzval  13694  lmbrf  15299  logge0b  15974  loggt0b  15975  logle1b  15976  loglt1b  15977  lgsne0  16140  lgsprme0  16144