Theorem exp42 611

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

Hypothesis

Ref	Expression
exp42.1

Assertion

Ref	Expression
exp42

Proof of Theorem exp42

Step	Hyp	Ref	Expression
1		exp42.1	. . 3
2	1	exp31 604	. 2
3	2	expd 436	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  isofrlem  6236  f1ocnv2d  6526  oelim  7203  zorn2lem7  8903  addid1  9781  issubg4  16220  lmodvsdir  17536  lmodvsass  17537  gsummatr01lem4  19160  dvfsumrlim3  22434  shscli  26235  f1o3d  27471  slmdvsdir  27759  slmdvsass  27760  initoeu1  32617  termoeu1  32624  lshpcmp  34713

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