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

Theorem impl 620
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 436 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 432 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 371
This theorem is referenced by:  sbc2iedv  3408  csbie2t  3464  ordelord  4900  frinxp  5064  foco2  6040  frxp  6893  mpt2curryd  6998  omsmolem  7302  erth  7356  unblem1  7771  unwdomg  8009  cflim2  8642  distrlem1pr  9402  uz11  11103  xmulge0  11475  max0add  13105  prmpwdvds  14280  imasleval  14795  resscntz  16171  ablfac1c  16921  lbsind  17521  mplcoe5lem  17917  isphld  18472  smadiadetr  18960  chfacfisf  19138  chfacfisfcpmat  19139  chcoeffeq  19170  cayhamlem3  19171  tx1stc  19902  ioorcl  21737  coemullem  22397  xrlimcnp  23042  fsumdvdscom  23205  fsumvma  23232  clwlkisclwwlklem2a  24477  clwwlkext2edg  24494  frg2wot1  24750  grpoidinvlem3  24900  htthlem  25526  atcvat4i  27008  abfmpeld  27180  isarchi3  27409  ordtconlem1  27558  funpartfun  29186  ltflcei  29636  neificl  29865  keridl  30048  mpaaeu  30720  lmod0rng  32049  lincext1  32145  cvrat4  34248  ps-2  34283
  Copyright terms: Public domain W3C validator