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

Theorem con3dimp 441
Description: Variant of con3d 133 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 133 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32imp 429 1  |-  ( (
ph  /\  -.  ch )  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  nelneq  2574  nelneq2  2575  nelss  3558  dtru  4647  sofld  5461  card2inf  7999  gchen1  9020  gchen2  9021  bcpasc  12402  fiinfnf1o  12426  hashfn  12446  swrdnd2  12669  swrdccat  12730  pcprod  14426  lubval  15741  glbval  15754  mplmonmul  18253  regr1lem  20366  blcld  21134  stdbdxmet  21144  itgss  22344  isosctrlem2  23279  isppw2  23515  dchrelbas3  23639  lgsdir  23731  rplogsum  23838  nb3graprlem2  24579  orngsqr  27955  qqhval2lem  28123  qqhf  28128  esumpinfval  28245  isfldidl  30670  jm2.23  31142  cncfiooicclem1  31899  fourierdlem81  32173  2f1fvneq  32571  bj-dtru  34526  lssat  34884  paddasslem1  35687  lcfrlem21  37433  hdmap10lem  37712  hdmap11lem2  37715
  Copyright terms: Public domain W3C validator