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

Theorem expl 618
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 604 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32impd 431 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> 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:  tfindsg2  6669  tz7.49c  7103  ssenen  7683  pssnn  7730  unwdomg  8001  cff1  8629  cfsmolem  8641  cfpwsdom  8950  wunex2  9107  mulgt0sr  9473  uzwo  11135  uzwoOLD  11136  shftfval  12855  fsum2dlem  13536  prmpwdvds  14272  divscrng  17665  chfacfscmul0  19121  chfacfpmmul0  19125  tgtop  19236  neitr  19442  bwth  19671  tx1stc  19881  cnextcn  20297  logfac2  23215  axcontlem12  23949  spanuni  26126  pjnmopi  26731  superpos  26937  atcvat4i  26980  fprod2dlem  28675  fin2so  29605  heicant  29615  ismblfin  29621  ovoliunnfl  29622  itg2gt0cn  29636  fneint  29738  neibastop3  29772  pell14qrexpcl  30396  cvrat4  34116
  Copyright terms: Public domain W3C validator