Theorem dedth3h 4538

Description: Weak deduction theorem eliminating three hypotheses. See comments in dedth2h 4537. (Contributed by NM, 15-May-1999.)

Hypotheses

Ref	Expression
dedth3h.1	⊢ (𝐴 = if(𝜑, 𝐴, 𝐷) → (𝜃 ↔ 𝜏))
dedth3h.2	⊢ (𝐵 = if(𝜓, 𝐵, 𝑅) → (𝜏 ↔ 𝜂))
dedth3h.3	⊢ (𝐶 = if(𝜒, 𝐶, 𝑆) → (𝜂 ↔ 𝜁))
dedth3h.4	⊢ 𝜁

Assertion

Ref	Expression
dedth3h	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem dedth3h

Step	Hyp	Ref	Expression
1		dedth3h.1	. . . 4 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐷) → (𝜃 ↔ 𝜏))
2	1	imbi2d 342	. . 3 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐷) → (((𝜓 ∧ 𝜒) → 𝜃) ↔ ((𝜓 ∧ 𝜒) → 𝜏)))
3		dedth3h.2	. . . 4 ⊢ (𝐵 = if(𝜓, 𝐵, 𝑅) → (𝜏 ↔ 𝜂))
4		dedth3h.3	. . . 4 ⊢ (𝐶 = if(𝜒, 𝐶, 𝑆) → (𝜂 ↔ 𝜁))
5		dedth3h.4	. . . 4 ⊢ 𝜁
6	3, 4, 5	dedth2h 4537	. . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜏)
7	2, 6	dedth 4536	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
8	7	3impib 1128	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1097   = wceq 1559  ifcif 4477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4478

This theorem is referenced by:  dedth3v  4541  faclbnd4lem2  14300  dvdsle  16334  gcdaddm  16549  ipdiri  30989  hvaddcan  31229  hvsubadd  31236  norm3dif  31309  omlsii  31562  chjass  31692  ledi  31699  spansncv  31812  pjcjt2  31851  pjopyth  31879  hoaddass  31941  hocsubdir  31944  hoddi  32149