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

Theorem expl 616
Description: Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.)
Hypothesis
Ref Expression
expl.1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
expl  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)

Proof of Theorem expl
StepHypRef Expression
1 expl.1 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
21exp31 602 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32impd 429 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  reximd2a  2873  tfindsg2  6678  tz7.49c  7147  ssenen  7728  pssnn  7772  unwdomg  8043  cff1  8669  cfsmolem  8681  cfpwsdom  8990  wunex2  9145  mulgt0sr  9511  uzwo  11189  shftfval  13050  fsum2dlem  13734  fprod2dlem  13934  prmpwdvds  14629  quscrng  18206  chfacfscmul0  19649  chfacfpmmul0  19653  tgtop  19765  neitr  19972  bwth  20201  tx1stc  20441  cnextcn  20857  logfac2  23871  axcontlem12  24682  spanuni  26862  pjnmopi  27466  superpos  27672  atcvat4i  27715  fpwrelmap  27989  2sqmo  28075  locfinreflem  28282  cmpcref  28292  fneint  30563  neibastop3  30577  isbasisrelowllem1  31259  isbasisrelowllem2  31260  relowlssretop  31266  fin2so  31392  heicant  31401  ismblfin  31407  ovoliunnfl  31408  itg2gt0cn  31423  cvrat4  32440  pell14qrexpcl  35144
  Copyright terms: Public domain W3C validator