Theorem exp42 639

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

Hypothesis

Ref	Expression
exp42.1	|- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ta )

Assertion

Ref	Expression
exp42	|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

Proof of Theorem exp42

Step	Hyp	Ref	Expression
1		exp42.1	. . 3 |- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ta )
2	1	exp31 630	. 2 |- ( ph -> ( ( ps /\ ch ) -> ( th -> ta ) ) )
3	2	expd 452	1 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  isofrlem  6590  f1ocnv2d  6886  oelim  7614  zorn2lem7  9324  addid1  10216  initoeu1  16661  termoeu1  16668  issubg4  17613  lmodvsdir  18887  lmodvsass  18888  gsummatr01lem4  20464  dvfsumrlim3  23796  shscli  28176  f1o3d  29431  slmdvsdir  29769  slmdvsass  29770  lshpcmp  34275