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  4429  ncfinraise  4482  nnpw1ex  4485  tfinltfinlem1  4501  sfintfin  4533  sfinltfin  4536  funfvima3  5462  isoini  5498  nchoicelem19  6308