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  1845  elrnmpt1  4985  xpopth  6344  sbcopeq1a  6355  ltnnnq  7648  ltaddsub  8621  leaddsub  8623  posdif  8640  lesub1  8641  ltsub1  8643  lesub0  8664  possumd  8754  subap0  8828  ltdivmul  9061  ledivmul  9062  zlem1lt  9541  zltlem1  9542  negelrp  9927  fzrev2  10325  fz1sbc  10336  elfzp1b  10337  qtri3or  10506  sumsqeq0  10886  sqrtle  11619  sqrtlt  11620  absgt0ap  11682  iser3shft  11929  dvdssubr  12423  gcdn0gt0  12572  divgcdcoprmex  12697  pcfac  12946  gsumfzval  13497  lmbrf  14968  logge0b  15643  loggt0b  15644  logle1b  15645  loglt1b  15646  lgsne0  15796  lgsprme0  15800