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

Theorem con3dimp 455
Description: Variant of con3d 146 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 146 . 2 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
32imp 443 1 ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  stoic1a  1687  nelneq  2711  nelneq2  2712  nelss  3626  dtru  4778  sofld  5486  card2inf  8320  gchen1  9303  gchen2  9304  bcpasc  12925  fiinfnf1o  12952  hashfn  12977  swrdnd2  13231  swrdccat  13290  nnoddn2prmb  15302  pcprod  15383  lubval  16753  glbval  16766  mplmonmul  19231  regr1lem  21294  blcld  22061  stdbdxmet  22071  itgss  23301  isosctrlem2  24266  isppw2  24558  dchrelbas3  24680  lgsdir  24774  2lgslem2  24837  2lgs  24849  rplogsum  24933  nb3graprlem2  25747  orngsqr  28941  qqhval2lem  29159  qqhf  29164  esumpinfval  29268  bj-dtru  31791  lindsenlbs  32370  poimirlem24  32399  isfldidl  32833  lssat  33117  paddasslem1  33920  lcfrlem21  35666  hdmap10lem  35945  hdmap11lem2  35948  jm2.23  36377  ntrneiel2  37200  ntrneik4w  37214  cncfiooicclem1  38576  fourierdlem81  38877  2f1fvneq  40131  nb3grprlem2  40604
  Copyright terms: Public domain W3C validator