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

Theorem expl 601
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 587 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp3a 420 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  tfindsg2  4755  tz7.49c  6600  ssenen  7178  pssnn  7224  unwdomg  7445  cff1  8031  cfsmolem  8043  cfpwsdom  8353  wunex2  8507  mulgt0sr  8874  uzwo  10432  uzwoOLD  10433  shftfval  11772  fsum2dlem  12441  prmpwdvds  13159  divscrng  16202  tgtop  16928  tx1stc  17561  logfac2  20679  spanuni  22557  pjnmopi  23162  superpos  23368  atcvat4i  23411  cnextcn  23824  axcontlem12  25430  ovoliunnfl  25756  itg2gt0cn  25763  fneint  25869  neibastop3  25903  pell14qrexpcl  26543  cvrat4  29691
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator