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  3060  csbie2t  3126  ordelord  4413  frinxp  4754  foco2  5642  frxp  6187  omsmolem  6647  erth  6700  unblem1  7105  unwdomg  7294  cflim2  7885  distrlem1pr  8645  uz11  10246  xmulge0  10600  max0add  11791  prmpwdvds  12947  imasleval  13439  resscntz  14803  ablfac1c  15302  lbsind  15829  isphld  16554  tx1stc  17340  ioorcl  18928  coemullem  19627  xrlimcnp  20259  fsumdvdscom  20421  fsumvma  20448  grpoidinvlem3  20867  htthlem  21491  atcvat4i  22973  axfelem20  23769  neificl  25878  keridl  26068  mpaaeu  26766  cvrat4  28911  ps-2  28946
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