Theorem imp41 593

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

Hypothesis

Ref	Expression
imp4.1

Assertion

Ref	Expression
imp41

Proof of Theorem imp41

Step	Hyp	Ref	Expression
1		imp4.1	. . 3
2	1	imp 429	. 2
3	2	imp31 432	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  3anassrs  1218  peano5  6723  oelim  7203  lemul12a  10425  uzwo  11173  uzwoOLD  11174  elfznelfzo  11915  injresinj  11926  swrdswrd  12685  2cshwcshw  12793  catidd  15077  grpinveu  16084  2ndcctbss  19956  erclwwlktr  24815  erclwwlkntr  24827  el2spthonot  24870  rusgranumwlks  24956  2pthfrgra  25011  frgrancvvdeqlemB  25038  2spotiundisj  25062  usg2spot2nb  25065  grpoinveu  25224  spansncvi  26570  sumdmdii  27334  unichnidl  30428  hbtlem2  31073  ply1mulgsumlem2  32987  ad4ant13  33224  ad4ant14  33225  ad4ant123  33226  ad4ant124  33227  ad4ant134  33228  ad4ant23  33229  ad4ant24  33230  ad4ant234  33231  ad5ant13  33233  ad5ant14  33234  ad5ant15  33235  ad5ant23  33236  ad5ant24  33237  ad5ant25  33238  ad5ant245  33239  ad5ant234  33240  ad5ant235  33241  ad5ant123  33242  ad5ant124  33243  ad5ant125  33244  ad5ant134  33245  ad5ant135  33246  ad5ant145  33247  ad5ant2345  33249  linepsubN  35476  pmapsub  35492  cdlemkid4  36660

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