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  890  drex1  1846  elrnmpt1  4983  xpopth  6339  sbcopeq1a  6350  ltnnnq  7643  ltaddsub  8616  leaddsub  8618  posdif  8635  lesub1  8636  ltsub1  8638  lesub0  8659  possumd  8749  subap0  8823  ltdivmul  9056  ledivmul  9057  zlem1lt  9536  zltlem1  9537  negelrp  9922  fzrev2  10320  fz1sbc  10331  elfzp1b  10332  qtri3or  10501  sumsqeq0  10881  sqrtle  11598  sqrtlt  11599  absgt0ap  11661  iser3shft  11908  dvdssubr  12402  gcdn0gt0  12551  divgcdcoprmex  12676  pcfac  12925  gsumfzval  13476  lmbrf  14942  logge0b  15617  loggt0b  15618  logle1b  15619  loglt1b  15620  lgsne0  15770  lgsprme0  15774