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

Theorem exp41 610
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 434 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  -> 
( th  ->  ta ) )
32exp31 604 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  tz7.49  7100  supxrun  11496  injresinj  11883  brfi1uzind  12485  swrdswrdlem  12634  swrdswrd  12635  2cshwcshw  12743  cshwcsh2id  12746  cusgrasize2inds  24139  usgra2adedgwlkonALT  24278  usgra2wlkspthlem2  24282  3v3e3cycl1  24306  constr3cycl  24323  4cycl4v4e  24328  4cycl4dv4e  24330  wwlknext  24386  wwlkextproplem3  24405  clwlkisclwwlklem2a4  24446  clwlkisclwwlklem1  24449  usghashecclwwlk  24497  clwlkfclwwlk  24506  el2wlkonot  24531  2spontn0vne  24549  rusgranumwlks  24618  1to3vfriswmgra  24669  frgranbnb  24682  frgrawopreg  24712  usg2spot2nb  24728  extwwlkfablem2  24741  numclwwlkovf2ex  24749  branmfn  26686  climrec  31100  usgra2pthspth  31775  usgra2pthlem1  31777  lincsumcl  31980  ad5ant1345  32202  ad5ant2345  32203  eel0001  32470  eel0000  32471  eel1111  32472  eel00001  32473  eel00000  32474  eel11111  32475
  Copyright terms: Public domain W3C validator