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  7790  ltaddsub  8765  leaddsub  8767  posdif  8784  lesub1  8785  ltsub1  8787  lesub0  8808  possumd  8899  subap0  8973  ltdivmul  9208  ledivmul  9209  zlem1lt  9705  zltlem1  9706  negelrp  10098  fzrev2  10502  fz1sbc  10513  elfzp1b  10514  qtri3or  10685  sumsqeq0  11068  sqrtle  11816  sqrtlt  11817  absgt0ap  11880  iser3shft  12128  dvdssubr  12622  gcdn0gt0  12771  divgcdcoprmex  12896  pcfac  13149  gzsumfzval  13760  lmbrf  15365  reaplog  16019  logge0b  16042  loggt0b  16043  logle1b  16044  loglt1b  16045  lgsne0  16276  lgsprme0  16280