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  888  drex1  1844  elrnmpt1  4981  xpopth  6334  sbcopeq1a  6345  ltnnnq  7633  ltaddsub  8606  leaddsub  8608  posdif  8625  lesub1  8626  ltsub1  8628  lesub0  8649  possumd  8739  subap0  8813  ltdivmul  9046  ledivmul  9047  zlem1lt  9526  zltlem1  9527  negelrp  9912  fzrev2  10310  fz1sbc  10321  elfzp1b  10322  qtri3or  10490  sumsqeq0  10870  sqrtle  11587  sqrtlt  11588  absgt0ap  11650  iser3shft  11897  dvdssubr  12390  gcdn0gt0  12539  divgcdcoprmex  12664  pcfac  12913  gsumfzval  13464  lmbrf  14929  logge0b  15604  loggt0b  15605  logle1b  15606  loglt1b  15607  lgsne0  15757  lgsprme0  15761