Theorem exp32 588

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

Hypothesis

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

Assertion

Ref	Expression
exp32	|- (ph -> (ps -> (ch -> th)))

Proof of Theorem exp32

Step	Hyp	Ref	Expression
1		exp32.1	. . 3 |- ((ph /\ (ps /\ ch)) -> th)
2	1	ex 423	. 2 |- (ph -> ((ps /\ ch) -> th))
3	2	exp3a 425	1 |- (ph -> (ps -> (ch -> th)))

Syntax hints:   -> wi 4   /\ wa 358

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 177  df-an 360

This theorem is referenced by:  exp44  596  exp45  597  expr  598  anassrs  629  an13s  778  3impb  1147  ax11eq  2193  ax11el  2194  nnsucelr  4428  ncfinraise  4481  nnpw1ex  4484  tfinltfinlem1  4500  sfintfin  4532  sfinltfin  4535  funfvima3  5461  isoini  5497  nchoicelem19  6307