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  4652  tz7.49c  6458  ssenen  7035  pssnn  7081  unwdomg  7298  cff1  7884  cfsmolem  7896  cfpwsdom  8206  wunex2  8360  mulgt0sr  8727  uzwo  10281  uzwoOLD  10282  shftfval  11565  fsum2dlem  12233  prmpwdvds  12951  divscrng  15992  tgtop  16711  tx1stc  17344  logfac2  20456  spanuni  22123  pjnmopi  22728  superpos  22934  atcvat4i  22977  axcontlem12  24603  fneint  26277  neibastop3  26311  pell14qrexpcl  26952  cvrat4  29632
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