Theorem bitr2d 188

Description: Deduction form of bitr2i 184. (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 187	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	3	bicomd 140	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitrrd  214  3bitr2rd  216  pm5.18dc  878  drex1  1791  elrnmpt1  4860  xpopth  6152  sbcopeq1a  6163  ltnnnq  7372  ltaddsub  8342  leaddsub  8344  posdif  8361  lesub1  8362  ltsub1  8364  lesub0  8385  possumd  8475  subap0  8549  ltdivmul  8779  ledivmul  8780  zlem1lt  9255  zltlem1  9256  negelrp  9631  fzrev2  10028  fz1sbc  10039  elfzp1b  10040  qtri3or  10186  sumsqeq0  10541  sqrtle  10987  sqrtlt  10988  absgt0ap  11050  iser3shft  11296  dvdssubr  11788  gcdn0gt0  11920  divgcdcoprmex  12043  pcfac  12289  lmbrf  12968  logge0b  13564  loggt0b  13565  logle1b  13566  loglt1b  13567  lgsne0  13692  lgsprme0  13696