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 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3bitrrd  215  3bitr2rd  217  pm5.18dc  895  drex1  1851  elrnmpt1  5033  xpopth  6410  sbcopeq1a  6421  ltnnnq  7791  ltaddsub  8766  leaddsub  8768  posdif  8785  lesub1  8786  ltsub1  8788  lesub0  8809  possumd  8900  subap0  8974  ltdivmul  9209  ledivmul  9210  zlem1lt  9706  zltlem1  9707  negelrp  10099  fzrev2  10503  fz1sbc  10514  elfzp1b  10515  qtri3or  10686  sumsqeq0  11070  sqrtle  11818  sqrtlt  11819  absgt0ap  11882  iser3shft  12131  dvdssubr  12625  gcdn0gt0  12774  divgcdcoprmex  12899  pcfac  13152  gzsumfzval  13764  lmbrf  15407  sineq0re  16042  reaplog  16063  logge0b  16086  loggt0b  16087  logle1b  16088  loglt1b  16089  bposlem7  16283  lgsne0  16328  lgsprme0  16332