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

Theorem con3and 428
Description: Variant of con3d 125 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 125 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32imp 418 1  |-  ( (
ph  /\  -.  ch )  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358
This theorem is referenced by:  ax12olem1  1868  nelneq  2381  nelneq2  2382  dtru  4201  posn  4758  frsn  4760  relimasn  5036  sofld  5121  card2inf  7269  gchen1  8247  gchen2  8248  bcpasc  11333  hashfn  11357  hashdomi  11362  pcprod  12943  mplmonmul  16208  regr1lem  17430  blcld  18051  stdbdxmet  18061  iblss  19159  itgss  19166  isosctrlem2  20119  isppw2  20353  dchrelbas3  20477  lgsdir  20569  rplogsum  20676  xaddeq0  23304  esumpinfval  23441  iintlem1  25610  isfldidl  26693  nelss  26751  jm2.23  27089  nssdmovg  28077  lssat  29206  paddasslem1  30009  lcfrlem21  31753  hdmap10lem  32032  hdmap11lem2  32035
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator