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  6493  tz7.49c  6922  ssenen  7506  pssnn  7552  unwdomg  7820  cff1  8448  cfsmolem  8460  cfpwsdom  8769  wunex2  8926  mulgt0sr  9293  uzwo  10938  uzwoOLD  10939  shftfval  12580  fsum2dlem  13258  prmpwdvds  13986  divscrng  17344  tgtop  18600  neitr  18806  bwth  19035  tx1stc  19245  cnextcn  19661  logfac2  22578  axcontlem12  23243  spanuni  24969  pjnmopi  25574  superpos  25780  atcvat4i  25823  fprod2dlem  27513  fin2so  28442  heicant  28452  ismblfin  28458  ovoliunnfl  28459  itg2gt0cn  28473  fneint  28575  neibastop3  28609  pell14qrexpcl  29234  cvrat4  33183
  Copyright terms: Public domain W3C validator