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

Theorem dedth3h 4285
Description: Weak deduction theorem eliminating three hypotheses. See comments in dedth2h 4284. (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 329 . . 3 (𝐴 = if(𝜑, 𝐴, 𝐷) → (((𝜓𝜒) → 𝜃) ↔ ((𝜓𝜒) → 𝜏)))
3 dedth3h.2 . . . 4 (𝐵 = if(𝜓, 𝐵, 𝑅) → (𝜏𝜂))
4 dedth3h.3 . . . 4 (𝐶 = if(𝜒, 𝐶, 𝑆) → (𝜂𝜁))
5 dedth3h.4 . . . 4 𝜁
63, 4, 5dedth2h 4284 . . 3 ((𝜓𝜒) → 𝜏)
72, 6dedth 4283 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
873impib 1109 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  ifcif 4230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-if 4231
This theorem is referenced by:  dedth3v  4288  faclbnd4lem2  13295  dvdsle  15254  gcdaddm  15468  ipdiri  28015  hvaddcan  28257  hvsubadd  28264  norm3dif  28337  omlsii  28592  chjass  28722  ledi  28729  spansncv  28842  pjcjt2  28881  pjopyth  28909  hoaddass  28971  hocsubdir  28974  hoddi  29179
  Copyright terms: Public domain W3C validator