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

Theorem expl 613
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 599 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp3a 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  6461  tz7.49c  6887  ssenen  7473  pssnn  7519  unwdomg  7787  cff1  8415  cfsmolem  8427  cfpwsdom  8736  wunex2  8892  mulgt0sr  9259  uzwo  10904  uzwoOLD  10905  shftfval  12542  fsum2dlem  13220  prmpwdvds  13947  divscrng  17243  tgtop  18419  neitr  18625  bwth  18854  tx1stc  19064  cnextcn  19480  logfac2  22440  axcontlem12  23043  spanuni  24769  pjnmopi  25374  superpos  25580  atcvat4i  25623  fprod2dlem  27337  fin2so  28257  heicant  28267  ismblfin  28273  ovoliunnfl  28274  itg2gt0cn  28288  fneint  28390  neibastop3  28424  pell14qrexpcl  29050  cvrat4  32657
  Copyright terms: Public domain W3C validator