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

Theorem dedth3h 4586
Description: Weak deduction theorem eliminating three hypotheses. See comments in dedth2h 4585. (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 4585 . . 3 ((𝜓𝜒) → 𝜏)
72, 6dedth 4584 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
873impib 1117 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  ifcif 4525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4526
This theorem is referenced by:  dedth3v  4589  faclbnd4lem2  14333  dvdsle  16347  gcdaddm  16562  ipdiri  30849  hvaddcan  31089  hvsubadd  31096  norm3dif  31169  omlsii  31422  chjass  31552  ledi  31559  spansncv  31672  pjcjt2  31711  pjopyth  31739  hoaddass  31801  hocsubdir  31804  hoddi  32009
  Copyright terms: Public domain W3C validator