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  1977  nelneq  2502  nelneq2  2503  dtru  4350  posn  4905  frsn  4907  relimasn  5186  sofld  5277  nssdmovg  6188  card2inf  7479  gchen1  8456  gchen2  8457  bcpasc  11567  fiinfnf1o  11589  hashfn  11604  hashdomi  11609  pcprod  13219  mplmonmul  16482  regr1lem  17724  blcld  18488  stdbdxmet  18498  iblss  19649  itgss  19656  isosctrlem2  20616  isppw2  20851  dchrelbas3  20975  lgsdir  21067  rplogsum  21174  nb3graprlem2  21414  xaddeq0  24072  xrge0npcan  24169  ofldsqr  24193  qqhval2lem  24318  qqhf  24323  esumpinfval  24416  hfext  26028  itg2addnclem2  26156  isfldidl  26568  nelss  26622  jm2.23  26957  2f1fvneq  27958  swrdccat3b  28031  lssat  29499  paddasslem1  30302  lcfrlem21  32046  hdmap10lem  32325  hdmap11lem2  32328
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