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  3072  csbie2t  3138  ordelord  4430  frinxp  4771  foco2  5696  frxp  6241  omsmolem  6667  erth  6720  unblem1  7125  unwdomg  7314  cflim2  7905  distrlem1pr  8665  uz11  10266  xmulge0  10620  max0add  11811  prmpwdvds  12967  imasleval  13459  resscntz  14823  ablfac1c  15322  lbsind  15849  isphld  16574  tx1stc  17360  ioorcl  18948  coemullem  19647  xrlimcnp  20279  fsumdvdscom  20441  fsumvma  20468  grpoidinvlem3  20889  htthlem  21513  atcvat4i  22993  funpartfun  24553  ltflcei  24998  neificl  26570  keridl  26760  mpaaeu  27458  cvrat4  30254  ps-2  30289
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