MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con3and Structured version   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  2011  nelneq  2534  nelneq2  2535  dtru  4383  posn  4939  frsn  4941  relimasn  5220  sofld  5311  nssdmovg  6222  card2inf  7516  gchen1  8493  gchen2  8494  bcpasc  11605  fiinfnf1o  11627  hashfn  11642  hashdomi  11647  pcprod  13257  mplmonmul  16520  regr1lem  17764  blcld  18528  stdbdxmet  18538  iblss  19689  itgss  19696  isosctrlem2  20656  isppw2  20891  dchrelbas3  21015  lgsdir  21107  rplogsum  21214  nb3graprlem2  21454  xaddeq0  24112  xrge0npcan  24209  ofldsqr  24233  qqhval2lem  24358  qqhf  24363  esumpinfval  24456  hfext  26117  itg2addnclem2  26248  isfldidl  26670  nelss  26724  jm2.23  27059  2f1fvneq  28064  swrdvalodm2  28161  swrdvalodm  28162  swrdccat  28183  lssat  29752  paddasslem1  30555  lcfrlem21  32299  hdmap10lem  32578  hdmap11lem2  32581
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