Theorem dedth3h 4522

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1092   = wceq 1547  ifcif 4461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-if 4462

This theorem is referenced by:  dedth3v  4525  faclbnd4lem2  14254  dvdsle  16277  gcdaddm  16492  ipdiri  30926  hvaddcan  31166  hvsubadd  31173  norm3dif  31246  omlsii  31499  chjass  31629  ledi  31636  spansncv  31749  pjcjt2  31788  pjopyth  31816  hoaddass  31878  hocsubdir  31881  hoddi  32086