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

Theorem exp41 613
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp41.1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ta )
Assertion
Ref Expression
exp41  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )

Proof of Theorem exp41
StepHypRef Expression
1 exp41.1 . . 3  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ta )
21ex 435 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  -> 
( th  ->  ta ) )
32exp31 607 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-an 372
This theorem is referenced by:  ad5ant2345  1255  tz7.49  7170  supxrun  11601  injresinj  12022  brfi1uzind  12641  swrdswrdlem  12800  swrdswrd  12801  2cshwcshw  12909  cshwcsh2id  12912  prmgaplem6  14989  cusgrasize2inds  25050  usgra2adedgwlkonALT  25189  usgra2wlkspthlem2  25193  3v3e3cycl1  25217  constr3cycl  25234  4cycl4v4e  25239  4cycl4dv4e  25241  wwlknext  25297  wwlkextproplem3  25316  clwlkisclwwlklem2a4  25357  clwlkisclwwlklem1  25360  usghashecclwwlk  25408  clwlkfclwwlk  25417  el2wlkonot  25442  2spontn0vne  25460  rusgranumwlks  25529  1to3vfriswmgra  25580  frgranbnb  25593  frgrawopreg  25622  usg2spot2nb  25638  extwwlkfablem2  25651  numclwwlkovf2ex  25659  branmfn  27593  relowlpssretop  31501  broucube  31681  eel0001  36748  eel0000  36749  eel1111  36750  eel00001  36751  eel00000  36752  eel11111  36753  climrec  37256  bgoldbtbndlem4  38305  bgoldbtbnd  38306  tgoldbach  38313  usgra2pthspth  38433  usgra2pthlem1  38435  usgra2pth  38436  2zlidl  38704  2zrngmmgm  38716  lincsumcl  38996
  Copyright terms: Public domain W3C validator