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  7636  ltaddsub  8609  leaddsub  8611  posdif  8628  lesub1  8629  ltsub1  8631  lesub0  8652  possumd  8742  subap0  8816  ltdivmul  9049  ledivmul  9050  zlem1lt  9529  zltlem1  9530  negelrp  9915  fzrev2  10313  fz1sbc  10324  elfzp1b  10325  qtri3or  10493  sumsqeq0  10873  sqrtle  11590  sqrtlt  11591  absgt0ap  11653  iser3shft  11900  dvdssubr  12393  gcdn0gt0  12542  divgcdcoprmex  12667  pcfac  12916  gsumfzval  13467  lmbrf  14932  logge0b  15607  loggt0b  15608  logle1b  15609  loglt1b  15610  lgsne0  15760  lgsprme0  15764