MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dedth3h Structured version   Visualization version   GIF version

Theorem dedth3h 4591
Description: Weak deduction theorem eliminating three hypotheses. See comments in dedth2h 4590. (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
StepHypRef Expression
1 dedth3h.1 . . . 4 (𝐴 = if(𝜑, 𝐴, 𝐷) → (𝜃𝜏))
21imbi2d 340 . . 3 (𝐴 = if(𝜑, 𝐴, 𝐷) → (((𝜓𝜒) → 𝜃) ↔ ((𝜓𝜒) → 𝜏)))
3 dedth3h.2 . . . 4 (𝐵 = if(𝜓, 𝐵, 𝑅) → (𝜏𝜂))
4 dedth3h.3 . . . 4 (𝐶 = if(𝜒, 𝐶, 𝑆) → (𝜂𝜁))
5 dedth3h.4 . . . 4 𝜁
63, 4, 5dedth2h 4590 . . 3 ((𝜓𝜒) → 𝜏)
72, 6dedth 4589 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
873impib 1115 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  ifcif 4531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-if 4532
This theorem is referenced by:  dedth3v  4594  faclbnd4lem2  14330  dvdsle  16344  gcdaddm  16559  ipdiri  30859  hvaddcan  31099  hvsubadd  31106  norm3dif  31179  omlsii  31432  chjass  31562  ledi  31569  spansncv  31682  pjcjt2  31721  pjopyth  31749  hoaddass  31811  hocsubdir  31814  hoddi  32019
  Copyright terms: Public domain W3C validator