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  7002  supxrun  11381  injresinj  11742  brfi1uzind  12323  swrdswrdlem  12457  swrdswrd  12458  cusgrasize2inds  23522  3v3e3cycl1  23667  constr3cycl  23684  4cycl4v4e  23689  4cycl4dv4e  23691  branmfn  25646  climrec  29916  usgra2pthspth  30435  usgra2wlkspthlem2  30437  usgra2pthlem1  30440  wwlknext  30496  el2wlkonot  30528  2spontn0vne  30546  clwlkisclwwlklem2a4  30586  clwlkisclwwlklem1  30589  erclwwlktr0  30619  cshwlemma1  30629  usghashecclwwlk  30649  clwlkfclwwlk  30657  wwlkextproplem3  30702  rusgranumwlks  30714  1to3vfriswmgra  30739  frgranbnb  30752  frgrawopreg  30782  usg2spot2nb  30798  extwwlkfablem2  30811  numclwwlkovf2ex  30819  scmatsubcl  31040  scmatmulcl  31042  lincsumcl  31074  ad5ant1345  31485  ad5ant2345  31486  eel0001  31753  eel0000  31754  eel1111  31755  eel00001  31756  eel00000  31757  eel11111  31758
  Copyright terms: Public domain W3C validator