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

Theorem con3and 429
Description: Variant of con3d 127 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 127 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32imp 419 1  |-  ( (
ph  /\  -.  ch )  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359
This theorem is referenced by:  ax12olem1OLD  1965  nelneq  2485  nelneq2  2486  dtru  4331  posn  4886  frsn  4888  relimasn  5167  sofld  5258  nssdmovg  6168  card2inf  7456  gchen1  8433  gchen2  8434  bcpasc  11539  fiinfnf1o  11561  hashfn  11576  hashdomi  11581  pcprod  13191  mplmonmul  16454  regr1lem  17692  blcld  18425  stdbdxmet  18435  iblss  19563  itgss  19570  isosctrlem2  20530  isppw2  20765  dchrelbas3  20889  lgsdir  20981  rplogsum  21088  nb3graprlem2  21327  xaddeq0  24030  xrge0npcan  24045  ofldsqr  24066  qqhval2lem  24164  qqhf  24169  esumpinfval  24259  hfext  25838  itg2addnclem2  25958  isfldidl  26369  nelss  26423  jm2.23  26758  lssat  29131  paddasslem1  29934  lcfrlem21  31678  hdmap10lem  31957  hdmap11lem2  31960
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 178  df-an 361
  Copyright terms: Public domain W3C validator