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  3145  csbie2t  3211  ordelord  4517  frinxp  4858  foco2  5791  frxp  6353  omsmolem  6793  erth  6846  unblem1  7256  unwdomg  7445  cflim2  8036  distrlem1pr  8796  uz11  10401  xmulge0  10756  max0add  12002  prmpwdvds  13159  imasleval  13653  resscntz  15017  ablfac1c  15516  lbsind  16043  isphld  16775  tx1stc  17561  ioorcl  19147  coemullem  19846  xrlimcnp  20485  fsumdvdscom  20648  fsumvma  20675  grpoidinvlem3  21305  htthlem  21931  atcvat4i  23411  funpartfun  25308  ltflcei  25753  neificl  26059  keridl  26248  mpaaeu  26946  cvrat4  29691  ps-2  29726
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