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

Theorem impl 618
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 )
)
21expd 434 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 430 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by:  sbc2iedv  3321  csbie2t  3377  ordelord  4814  frinxp  4979  foco2  5953  frxp  6809  mpt2curryd  6916  omsmolem  7220  erth  7274  unblem1  7687  unwdomg  7925  cflim2  8556  distrlem1pr  9314  uz11  11023  xmulge0  11397  max0add  13145  prmpwdvds  14424  imasleval  14948  resscntz  16486  ablfac1c  17235  lbsind  17839  mplcoe5lem  18243  cply1mul  18448  isphld  18780  smadiadetr  19262  chfacfisf  19440  chfacfisfcpmat  19441  chcoeffeq  19472  cayhamlem3  19473  tx1stc  20236  ioorcl  22071  coemullem  22732  xrlimcnp  23415  fsumdvdscom  23578  fsumvma  23605  clwlkisclwwlklem2a  24906  clwwlkext2edg  24923  frg2wot1  25178  grpoidinvlem3  25325  htthlem  25951  atcvat4i  27432  abfmpeld  27632  isarchi3  27884  ordtconlem1  28060  funpartfun  29746  ltflcei  30208  neificl  30412  keridl  30595  mpaaeu  31267  lmod0rng  32874  lincext1  33255  cvrat4  35580  ps-2  35615
  Copyright terms: Public domain W3C validator