Theorem bitr2d 187

Description: Deduction form of bitr2i 183. (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 186	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	3	bicomd 139	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3bitrrd  213  3bitr2rd  215  pm5.18dc  810  drex1  1719  elrnmpt1  4603  xpopth  5822  sbcopeq1a  5833  ltnnnq  6613  ltaddsub  7540  leaddsub  7542  posdif  7559  lesub1  7560  ltsub1  7562  lesub0  7583  possumd  7669  ltdivmul  7954  ledivmul  7955  zlem1lt  8407  zltlem1  8408  fzrev2  9102  fz1sbc  9113  elfzp1b  9114  qtri3or  9252  sumsqeq0  9554  sqrtle  9922  sqrtlt  9923  absgt0ap  9985  dvdssubr  10241  gcdn0gt0  10369  divgcdcoprmex  10484