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

Theorem con3dimp 442
Description: Variant of con3d 138 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
con3dimp.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
con3dimp  |-  ( (
ph  /\  -.  ch )  ->  -.  ps )

Proof of Theorem con3dimp
StepHypRef Expression
1 con3dimp.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21con3d 138 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32imp 430 1  |-  ( (
ph  /\  -.  ch )  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-an 372
This theorem is referenced by:  nelneq  2546  nelneq2  2547  nelss  3529  dtru  4616  sofld  5304  card2inf  8070  gchen1  9049  gchen2  9050  bcpasc  12503  fiinfnf1o  12530  hashfn  12551  swrdnd2  12774  swrdccat  12834  pcprod  14803  lubval  16181  glbval  16194  mplmonmul  18623  regr1lem  20685  blcld  21451  stdbdxmet  21461  itgss  22646  isosctrlem2  23613  isppw2  23905  dchrelbas3  24029  lgsdir  24121  rplogsum  24228  nb3graprlem2  25025  orngsqr  28406  qqhval2lem  28624  qqhf  28629  esumpinfval  28733  bj-dtru  31163  poimirlem24  31667  isfldidl  32004  lssat  32290  paddasslem1  33093  lcfrlem21  34839  hdmap10lem  35118  hdmap11lem2  35121  jm2.23  35556  cncfiooicclem1  37342  fourierdlem81  37618  2f1fvneq  38383
  Copyright terms: Public domain W3C validator