Theorem imp42 594

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

Hypothesis

Ref	Expression
imp4.1

Assertion

Ref	Expression
imp42

Proof of Theorem imp42

Step	Hyp	Ref	Expression
1		imp4.1	. . 3
2	1	imp32 433	. 2
3	2	imp 429	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  imp55  601  ltexprlem7  9441  iscatd  15070  isposd  15585  pospropd  15764  mulgghm2  18531  mulgghm2OLD  18534  ordtbaslem  19689  txbas  20068  grporcan  25223  chirredlem1  27309  cvxpcon  28687  cvxscon  28688  nocvxminlem  29450  rngonegmn1l  30352  prnc  30464

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