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

Theorem con3dimp 457
 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 445 1 ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 384 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 386 This theorem is referenced by:  stoic1a  1695  nelneq  2723  nelneq2  2724  nelss  3656  dtru  4848  sofld  5569  2f1fvneq  6502  card2inf  8445  gchen1  9432  gchen2  9433  bcpasc  13091  fiinfnf1o  13121  hashfn  13147  swrdnd2  13415  swrdccat  13474  nnoddn2prmb  15499  pcprod  15580  lubval  16965  glbval  16978  mplmonmul  19445  regr1lem  21523  blcld  22291  stdbdxmet  22301  itgss  23559  isosctrlem2  24530  isppw2  24822  dchrelbas3  24944  lgsdir  25038  2lgslem2  25101  2lgs  25113  rplogsum  25197  nb3grprlem2  26264  orngsqr  29778  qqhval2lem  29999  qqhf  30004  esumpinfval  30109  bj-dtru  32772  lindsenlbs  33375  poimirlem24  33404  isfldidl  33838  lssat  34122  paddasslem1  34925  lcfrlem21  36671  hdmap10lem  36950  hdmap11lem2  36953  jm2.23  37382  ntrneiel2  38204  ntrneik4w  38218  cncfiooicclem1  39869  fourierdlem81  40167
 Copyright terms: Public domain W3C validator