Theorem dedth3h 4544

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1563  ifcif 4483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4484

This theorem is referenced by:  dedth3v  4547  faclbnd4lem2  14318  dvdsle  16356  gcdaddm  16571  ipdiri  31087  hvaddcan  31327  hvsubadd  31334  norm3dif  31407  omlsii  31660  chjass  31790  ledi  31797  spansncv  31910  pjcjt2  31949  pjopyth  31977  hoaddass  32039  hocsubdir  32042  hoddi  32247