Theorem exp41 610

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
exp41.1

Assertion

Ref	Expression
exp41

Proof of Theorem exp41

Step	Hyp	Ref	Expression
1		exp41.1	. . 3
2	1	ex 434	. 2
3	2	exp31 604	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  tz7.49  7129  supxrun  11536  injresinj  11926  brfi1uzind  12532  swrdswrdlem  12684  swrdswrd  12685  2cshwcshw  12793  cshwcsh2id  12796  cusgrasize2inds  24477  usgra2adedgwlkonALT  24616  usgra2wlkspthlem2  24620  3v3e3cycl1  24644  constr3cycl  24661  4cycl4v4e  24666  4cycl4dv4e  24668  wwlknext  24724  wwlkextproplem3  24743  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem1  24787  usghashecclwwlk  24835  clwlkfclwwlk  24844  el2wlkonot  24869  2spontn0vne  24887  rusgranumwlks  24956  1to3vfriswmgra  25007  frgranbnb  25020  frgrawopreg  25049  usg2spot2nb  25065  extwwlkfablem2  25078  numclwwlkovf2ex  25086  branmfn  27024  climrec  31609  usgra2pthspth  32351  usgra2pthlem1  32353  usgra2pth  32354  2zlidl  32740  2zrngmmgm  32752  lincsumcl  33032  ad5ant2345  33249  eel0001  33515  eel0000  33516  eel1111  33517  eel00001  33518  eel00000  33519  eel11111  33520

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