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  2534  nelneq2  2535  nelss  3523  dtru  4615  sofld  5303  card2inf  8079  gchen1  9057  gchen2  9058  bcpasc  12512  fiinfnf1o  12539  hashfn  12560  swrdnd2  12791  swrdccat  12851  pcprod  14839  lubval  16229  glbval  16242  mplmonmul  18687  regr1lem  20752  blcld  21518  stdbdxmet  21528  itgss  22767  isosctrlem2  23746  isppw2  24040  dchrelbas3  24164  lgsdir  24256  rplogsum  24363  nb3graprlem2  25178  orngsqr  28575  qqhval2lem  28793  qqhf  28798  esumpinfval  28902  bj-dtru  31382  poimirlem24  31928  isfldidl  32265  lssat  32551  paddasslem1  33354  lcfrlem21  35100  hdmap10lem  35379  hdmap11lem2  35382  jm2.23  35821  cncfiooicclem1  37711  fourierdlem81  37991  2f1fvneq  38877  nb3grprlem2  39215
  Copyright terms: Public domain W3C validator