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

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

Proof of Theorem con3and
StepHypRef Expression
1 con3and.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21con3d 133 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32imp 429 1  |-  ( (
ph  /\  -.  ch )  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  nelneq  2539  nelneq2  2540  nelss  3412  dtru  4480  posn  4903  frsn  4905  relimasn  5189  sofld  5283  nssdmovg  6244  card2inf  7766  gchen1  8788  gchen2  8789  bcpasc  12093  fiinfnf1o  12117  hashfn  12134  hashdomi  12139  swrdvalodm2  12329  swrdvalodm  12330  swrdccat  12380  pcprod  13953  lubval  15150  glbval  15163  mplmonmul  17521  regr1lem  19271  blcld  20039  stdbdxmet  20049  iblss  21241  itgss  21248  isosctrlem2  22176  isppw2  22412  dchrelbas3  22536  lgsdir  22628  rplogsum  22735  nb3graprlem2  23295  xaddeq0  25981  xrge0npcan  26090  qqhval2lem  26346  qqhf  26351  esumpinfval  26458  hfext  28150  itg2addnclem2  28369  dvasin  28405  isfldidl  28793  jm2.23  29270  2f1fvneq  30068  bj-dtru  32078  lssat  32383  paddasslem1  33186  lcfrlem21  34930  hdmap10lem  35209  hdmap11lem2  35212
  Copyright terms: Public domain W3C validator