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  884  drex1  1812  elrnmpt1  4918  xpopth  6243  sbcopeq1a  6254  ltnnnq  7509  ltaddsub  8482  leaddsub  8484  posdif  8501  lesub1  8502  ltsub1  8504  lesub0  8525  possumd  8615  subap0  8689  ltdivmul  8922  ledivmul  8923  zlem1lt  9401  zltlem1  9402  negelrp  9781  fzrev2  10179  fz1sbc  10190  elfzp1b  10191  qtri3or  10349  sumsqeq0  10729  sqrtle  11220  sqrtlt  11221  absgt0ap  11283  iser3shft  11530  dvdssubr  12023  gcdn0gt0  12172  divgcdcoprmex  12297  pcfac  12546  gsumfzval  13095  lmbrf  14537  logge0b  15212  loggt0b  15213  logle1b  15214  loglt1b  15215  lgsne0  15365  lgsprme0  15369