Theorem dedth3h 4608

Description: Weak deduction theorem eliminating three hypotheses. See comments in dedth2h 4607. (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 340	. . 3 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐷) → (((𝜓 ∧ 𝜒) → 𝜃) ↔ ((𝜓 ∧ 𝜒) → 𝜏)))
3		dedth3h.2	. . . 4 ⊢ (𝐵 = if(𝜓, 𝐵, 𝑅) → (𝜏 ↔ 𝜂))
4		dedth3h.3	. . . 4 ⊢ (𝐶 = if(𝜒, 𝐶, 𝑆) → (𝜂 ↔ 𝜁))
5		dedth3h.4	. . . 4 ⊢ 𝜁
6	3, 4, 5	dedth2h 4607	. . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜏)
7	2, 6	dedth 4606	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
8	7	3impib 1116	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-if 4549

This theorem is referenced by:  dedth3v  4611  faclbnd4lem2  14343  dvdsle  16358  gcdaddm  16571  ipdiri  30862  hvaddcan  31102  hvsubadd  31109  norm3dif  31182  omlsii  31435  chjass  31565  ledi  31572  spansncv  31685  pjcjt2  31724  pjopyth  31752  hoaddass  31814  hocsubdir  31817  hoddi  32022