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

Theorem con3dimp 412
Description: Variant of con3d 155 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 155 . 2 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
32imp 410 1 ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  stoic1a  1774  nelneq  2940  nelneq2  2941  nelss  4016  eldifsnneqOLD  4709  dtru  5259  sofld  6032  2f1fvneq  7008  card2inf  9012  gchen1  10041  gchen2  10042  bcpasc  13684  fiinfnf1o  13713  hashfn  13739  swrdnd2  14015  swrdccat  14095  nnoddn2prmb  16146  pcprod  16227  lubval  17592  glbval  17605  mplmonmul  20240  regr1lem  22342  blcld  23110  stdbdxmet  23120  itgss  24413  isosctrlem2  25403  isppw2  25698  dchrelbas3  25820  lgsdir  25914  2lgslem2  25977  2lgs  25989  rplogsum  26109  nb3grprlem2  27169  orngsqr  30904  qqhval2lem  31249  qqhf  31254  esumpinfval  31359  spthcycl  32403  bj-dtru  34168  lindsenlbs  34964  poimirlem24  34993  isfldidl  35418  lssat  36224  paddasslem1  37028  lcfrlem21  38771  hdmap10lem  39047  hdmap11lem2  39050  jm2.23  39793  ntrneiel2  40648  ntrneik4w  40662  cncfiooicclem1  42401  fourierdlem81  42695
  Copyright terms: Public domain W3C validator