MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  expl 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  4800  tz7.49c  6662  ssenen  7240  pssnn  7286  unwdomg  7508  cff1  8094  cfsmolem  8106  cfpwsdom  8415  wunex2  8569  mulgt0sr  8936  uzwo  10495  uzwoOLD  10496  shftfval  11840  fsum2dlem  12509  prmpwdvds  13227  divscrng  16266  tgtop  16993  neitr  17198  tx1stc  17635  cnextcn  18051  logfac2  20954  spanuni  22999  pjnmopi  23604  superpos  23810  atcvat4i  23853  fprod2dlem  25257  axcontlem12  25818  ismblfin  26146  ovoliunnfl  26147  itg2gt0cn  26159  fneint  26247  neibastop3  26281  pell14qrexpcl  26820  cvrat4  29925
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