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

Theorem impl 603
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 425 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 421 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  sbc2iedv  3061  csbie2t  3127  ordelord  4416  frinxp  4757  foco2  5682  frxp  6227  omsmolem  6653  erth  6706  unblem1  7111  unwdomg  7300  cflim2  7891  distrlem1pr  8651  uz11  10252  xmulge0  10606  max0add  11797  prmpwdvds  12953  imasleval  13445  resscntz  14809  ablfac1c  15308  lbsind  15835  isphld  16560  tx1stc  17346  ioorcl  18934  coemullem  19633  xrlimcnp  20265  fsumdvdscom  20427  fsumvma  20454  grpoidinvlem3  20875  htthlem  21499  atcvat4i  22979  ltflcei  24930  neificl  26478  keridl  26668  mpaaeu  27366  cvrat4  29705  ps-2  29740
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 177  df-an 360
  Copyright terms: Public domain W3C validator