Theorem imp4a 589

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

Hypothesis

Ref	Expression
imp4.1

Assertion

Ref	Expression
imp4a

Proof of Theorem imp4a

Step	Hyp	Ref	Expression
1		imp4.1	. 2
2		impexp 446	. 2
3	1, 2	syl6ibr 227	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  imp4b  590  imp4d  592  imp55  601  imp511  602  reuss2  3777  wefrc  4878  f1oweALT  6784  tfrlem9  7073  tz7.49  7129  oaordex  7226  dfac2  8532  zorn2lem4  8900  zorn2lem7  8903  psslinpr  9430  facwordi  12367  ndvdssub  14065  pmtrfrn  16483  elcls  19574  elcls3  19584  neibl  21004  met2ndc  21026  itgcn  22249  branmfn  27024  atcvatlem  27304  atcvat4i  27316  prtlem15  30616  cvlsupr4  35070  cvlsupr5  35071  cvlsupr6  35072  2llnneN  35133  cvrat4  35167  llnexchb2  35593  cdleme48gfv1  36262  cdlemg6e  36348  dihord6apre  36983  dihord5b  36986  dihord5apre  36989  dihglblem5apreN  37018  dihglbcpreN  37027

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