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  1880  nelneq  2394  nelneq2  2395  dtru  4217  posn  4774  frsn  4776  relimasn  5052  sofld  5137  card2inf  7285  gchen1  8263  gchen2  8264  bcpasc  11349  hashfn  11373  hashdomi  11378  pcprod  12959  mplmonmul  16224  regr1lem  17446  blcld  18067  stdbdxmet  18077  iblss  19175  itgss  19182  isosctrlem2  20135  isppw2  20369  dchrelbas3  20493  lgsdir  20585  rplogsum  20692  xaddeq0  23319  esumpinfval  23456  itg2addnclem2  25004  iintlem1  25713  isfldidl  26796  nelss  26854  jm2.23  27192  nssdmovg  28194  nb3graprlem2  28288  lssat  29828  paddasslem1  30631  lcfrlem21  32375  hdmap10lem  32654  hdmap11lem2  32657
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