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

Theorem dedth3h 4091
 Description: Weak deduction theorem eliminating three hypotheses. See comments in dedth2h 4090. (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 4090 . . 3 ((𝜓𝜒) → 𝜏)
72, 6dedth 4089 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
873impib 1254 1 ((𝜑𝜓𝜒) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ifcif 4036 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037 This theorem is referenced by:  dedth3v  4094  faclbnd4lem2  12943  dvdsle  14870  gcdaddm  15084  ipdiri  27069  hvaddcan  27311  hvsubadd  27318  norm3dif  27391  omlsii  27646  chjass  27776  ledi  27783  spansncv  27896  pjcjt2  27935  pjopyth  27963  hoaddass  28025  hocsubdir  28028  hoddi  28233
 Copyright terms: Public domain W3C validator