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

Theorem con3dimp 408
Description: Variant of con3d 152 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 152 . 2 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
32imp 406 1 ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  stoic1a  1772  nelneq  2865  nelneq2  2866  nelss  4049  dtruALT2  5370  dtruOLD  5446  sofld  6207  2f1fvneq  7280  card2inf  9595  gchen1  10665  gchen2  10666  bcpasc  14360  fiinfnf1o  14389  hashfn  14414  swrdnd2  14693  swrdccat  14773  nnoddn2prmb  16851  pcprod  16933  lubval  18401  glbval  18414  mplmonmul  22054  regr1lem  23747  blcld  24518  stdbdxmet  24528  itgss  25847  isosctrlem2  26862  isppw2  27158  dchrelbas3  27282  lgsdir  27376  2lgslem2  27439  2lgs  27451  rplogsum  27571  nb3grprlem2  29398  orngsqr  33334  qqhval2lem  33982  qqhf  33987  esumpinfval  34074  spthcycl  35134  lindsenlbs  37622  poimirlem24  37651  isfldidl  38075  lssat  39017  paddasslem1  39822  lcfrlem21  41565  hdmap10lem  41841  hdmap11lem2  41844  fsuppssind  42603  jm2.23  43008  ntrneiel2  44099  ntrneik4w  44113  cncfiooicclem1  45908  fourierdlem81  46202
  Copyright terms: Public domain W3C validator