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 206  df-an 396
This theorem is referenced by:  stoic1a  1767  nelneq  2852  nelneq2  2853  nelss  4043  dtruALT2  5364  dtruOLD  5437  sofld  6185  2f1fvneq  7264  card2inf  9570  gchen1  10640  gchen2  10641  bcpasc  14304  fiinfnf1o  14333  hashfn  14358  swrdnd2  14629  swrdccat  14709  nnoddn2prmb  16773  pcprod  16855  lubval  18339  glbval  18352  mplmonmul  21961  regr1lem  23630  blcld  24401  stdbdxmet  24411  itgss  25728  isosctrlem2  26738  isppw2  27034  dchrelbas3  27158  lgsdir  27252  2lgslem2  27315  2lgs  27327  rplogsum  27447  nb3grprlem2  29181  orngsqr  32959  qqhval2lem  33518  qqhf  33523  esumpinfval  33628  spthcycl  34675  lindsenlbs  37023  poimirlem24  37052  isfldidl  37476  lssat  38425  paddasslem1  39230  lcfrlem21  40973  hdmap10lem  41249  hdmap11lem2  41252  fsuppssind  41748  jm2.23  42339  ntrneiel2  43439  ntrneik4w  43453  cncfiooicclem1  45204  fourierdlem81  45498
  Copyright terms: Public domain W3C validator