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  3263  csbie2t  3316  ordelord  4741  frinxp  4904  foco2  5863  frxp  6682  mpt2curryd  6788  omsmolem  7092  erth  7145  unblem1  7564  unwdomg  7799  cflim2  8432  distrlem1pr  9194  uz11  10883  xmulge0  11247  max0add  12799  prmpwdvds  13965  imasleval  14479  resscntz  15849  ablfac1c  16572  lbsind  17161  mplcoe5lem  17547  isphld  18083  smadiadetr  18481  tx1stc  19223  ioorcl  21057  coemullem  21717  xrlimcnp  22362  fsumdvdscom  22525  fsumvma  22552  grpoidinvlem3  23693  htthlem  24319  atcvat4i  25801  abfmpeld  25969  isarchi3  26204  ordtconlem1  26354  funpartfun  27974  ltflcei  28419  neificl  28649  keridl  28832  mpaaeu  29507  clwlkisclwwlklem2a  30447  clwwlkext2edg  30464  frg2wot1  30650  lmod0rng  30779  lincext1  30988  cvrat4  33087  ps-2  33122
  Copyright terms: Public domain W3C validator