MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  impl Structured version   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  3229  csbie2t  3295  ordelord  4603  frinxp  4943  foco2  5889  frxp  6456  omsmolem  6896  erth  6949  unblem1  7359  unwdomg  7552  cflim2  8143  distrlem1pr  8902  uz11  10508  xmulge0  10863  max0add  12115  prmpwdvds  13272  imasleval  13766  resscntz  15130  ablfac1c  15629  lbsind  16152  isphld  16885  tx1stc  17682  ioorcl  19469  coemullem  20168  xrlimcnp  20807  fsumdvdscom  20970  fsumvma  20997  grpoidinvlem3  21794  htthlem  22420  atcvat4i  23900  abfmpeld  24066  sibfof  24654  funpartfun  25788  ltflcei  26239  neificl  26459  keridl  26642  mpaaeu  27332  cshwsame  28277  frg2wot1  28446  cvrat4  30240  ps-2  30275
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