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

Theorem impl 604
Description: Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.)
Hypothesis
Ref Expression
impl.1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
impl  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )

Proof of Theorem impl
StepHypRef Expression
1 impl.1 . . 3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
21exp3a 426 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 422 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  sbc2iedv  3216  csbie2t  3282  ordelord  4590  frinxp  4929  foco2  5875  frxp  6442  omsmolem  6882  erth  6935  unblem1  7345  unwdomg  7536  cflim2  8127  distrlem1pr  8886  uz11  10492  xmulge0  10847  max0add  12098  prmpwdvds  13255  imasleval  13749  resscntz  15113  ablfac1c  15612  lbsind  16135  isphld  16868  tx1stc  17665  ioorcl  19452  coemullem  20151  xrlimcnp  20790  fsumdvdscom  20953  fsumvma  20980  grpoidinvlem3  21777  htthlem  22403  atcvat4i  23883  abfmpeld  24049  sibfof  24637  funpartfun  25733  ltflcei  26182  neificl  26391  keridl  26574  mpaaeu  27265  frg2wot1  28202  cvrat4  29971  ps-2  30006
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