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

Theorem expl 602
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 588 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp3a 421 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  tfindsg2  4841  tz7.49c  6703  ssenen  7281  pssnn  7327  unwdomg  7552  cff1  8138  cfsmolem  8150  cfpwsdom  8459  wunex2  8613  mulgt0sr  8980  uzwo  10539  uzwoOLD  10540  shftfval  11885  fsum2dlem  12554  prmpwdvds  13272  divscrng  16311  tgtop  17038  neitr  17244  tx1stc  17682  cnextcn  18098  logfac2  21001  spanuni  23046  pjnmopi  23651  superpos  23857  atcvat4i  23900  fprod2dlem  25304  axcontlem12  25914  ismblfin  26247  ovoliunnfl  26248  itg2gt0cn  26260  fneint  26357  neibastop3  26391  pell14qrexpcl  26930  cvrat4  30240
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 178  df-an 361
  Copyright terms: Public domain W3C validator