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

Theorem con3dimp 456
Description: Variant of con3d 148 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
con3dimp.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
con3dimp ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓)

Proof of Theorem con3dimp
StepHypRef Expression
1 con3dimp.1 . . 3 (𝜑 → (𝜓𝜒))
21con3d 148 . 2 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
32imp 444 1 ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  stoic1a  1737  nelneq  2754  nelneq2  2755  nelss  3697  dtru  4887  sofld  5616  2f1fvneq  6557  card2inf  8501  gchen1  9485  gchen2  9486  bcpasc  13148  fiinfnf1o  13178  hashfn  13202  swrdnd2  13479  swrdccat  13539  nnoddn2prmb  15565  pcprod  15646  lubval  17031  glbval  17044  mplmonmul  19512  regr1lem  21590  blcld  22357  stdbdxmet  22367  itgss  23623  isosctrlem2  24594  isppw2  24886  dchrelbas3  25008  lgsdir  25102  2lgslem2  25165  2lgs  25177  rplogsum  25261  nb3grprlem2  26327  orngsqr  29932  qqhval2lem  30153  qqhf  30158  esumpinfval  30263  bj-dtru  32922  lindsenlbs  33534  poimirlem24  33563  isfldidl  33997  lssat  34621  paddasslem1  35424  lcfrlem21  37169  hdmap10lem  37448  hdmap11lem2  37451  jm2.23  37880  ntrneiel2  38701  ntrneik4w  38715  cncfiooicclem1  40424  fourierdlem81  40722
  Copyright terms: Public domain W3C validator