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

Theorem con3dimp 447
Description: Variant of con3d 140 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
con3dimp.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
con3dimp  |-  ( (
ph  /\  -.  ch )  ->  -.  ps )

Proof of Theorem con3dimp
StepHypRef Expression
1 con3dimp.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21con3d 140 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32imp 435 1  |-  ( (
ph  /\  -.  ch )  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  nelneq  2564  nelneq2  2565  nelss  3503  dtru  4611  sofld  5306  card2inf  8101  gchen1  9081  gchen2  9082  bcpasc  12544  fiinfnf1o  12571  hashfn  12592  swrdnd2  12832  swrdccat  12892  pcprod  14895  lubval  16285  glbval  16298  mplmonmul  18743  regr1lem  20809  blcld  21575  stdbdxmet  21585  itgss  22825  isosctrlem2  23804  isppw2  24098  dchrelbas3  24222  lgsdir  24314  rplogsum  24421  nb3graprlem2  25236  orngsqr  28618  qqhval2lem  28836  qqhf  28841  esumpinfval  28945  bj-dtru  31458  poimirlem24  32010  isfldidl  32347  lssat  32628  paddasslem1  33431  lcfrlem21  35177  hdmap10lem  35456  hdmap11lem2  35459  jm2.23  35897  cncfiooicclem1  37857  fourierdlem81  38152  2f1fvneq  39150  nb3grprlem2  39601
  Copyright terms: Public domain W3C validator