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  3059  csbie2t  3125  ordelord  4414  frinxp  4755  foco2  5680  frxp  6225  omsmolem  6651  erth  6704  unblem1  7109  unwdomg  7298  cflim2  7889  distrlem1pr  8649  uz11  10250  xmulge0  10604  max0add  11795  prmpwdvds  12951  imasleval  13443  resscntz  14807  ablfac1c  15306  lbsind  15833  isphld  16558  tx1stc  17344  ioorcl  18932  coemullem  19631  xrlimcnp  20263  fsumdvdscom  20425  fsumvma  20452  grpoidinvlem3  20873  htthlem  21497  atcvat4i  22977  neificl  26467  keridl  26657  mpaaeu  27355  cvrat4  29632  ps-2  29667
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