Theorem imp43 595

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

Hypothesis

Ref	Expression
imp4.1

Assertion

Ref	Expression
imp43

Proof of Theorem imp43

Step	Hyp	Ref	Expression
1		imp4.1	. . 3
2	1	imp4b 590	. 2
3	2	imp 429	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  sotriOLD  5404  fundmen  7609  fiint  7817  ltexprlem6  9440  divgt0  10435  divge0  10436  le2sq2  12243  iscatd  15070  isfuncd  15234  islmodd  17518  lmodvsghm  17571  islssd  17582  basis2  19452  neindisj  19618  dvidlem  22319  spansneleq  26488  elspansn4  26491  adjmul  27011  kbass6  27040  mdsl0  27229  chirredlem1  27309  rngonegmn1r  30353  3dim1  35191  linepsubN  35476  pmapsub  35492

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