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  8764  leaddsub  8766  posdif  8783  lesub1  8784  ltsub1  8786  lesub0  8807  possumd  8897  subap0  8971  ltdivmul  9206  ledivmul  9207  zlem1lt  9701  zltlem1  9702  negelrp  10088  fzrev2  10492  fz1sbc  10503  elfzp1b  10504  qtri3or  10675  sumsqeq0  11055  sqrtle  11802  sqrtlt  11803  absgt0ap  11865  iser3shft  12112  dvdssubr  12606  gcdn0gt0  12755  divgcdcoprmex  12880  pcfac  13129  gzsumfzval  13711  lmbrf  15316  reaplog  15970  logge0b  15993  loggt0b  15994  logle1b  15995  loglt1b  15996  lgsne0  16161  lgsprme0  16165