Theorem exp3a 425

Description: Exportation deduction. (Contributed by NM, 20-Aug-1993.)

Hypothesis

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

Assertion

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

Proof of Theorem exp3a

Step	Hyp	Ref	Expression
1		exp3a.1	. . . 4 |- (ph -> ((ps /\ ch) -> th))
2	1	com12 27	. . 3 |- ((ps /\ ch) -> (ph -> th))
3	2	ex 423	. 2 |- (ps -> (ch -> (ph -> th)))
4	3	com3r 73	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:  expdimp  426  pm3.3  431  syland  467  exp32  588  exp4c  591  exp4d  592  exp42  594  exp44  596  exp5c  599  impl  603  mpan2d  655  3impib  1149  exp5o  1170  exbir  1365  exp3acom3r  1370  exp3acom23  1372  nfsb4t  2080  ax11indn  2195  mo  2226  mopick  2266  ralrimivv  2706  mob2  3017  reuind  3040  reupick3  3541  pwadjoin  4120  opkthg  4132  nndisjeq  4430  ssfin  4471  ncfinraise  4482  sfin112  4530  sfintfin  4533  vfinspss  4552  phi11lem1  4596  funcnvuni  5162  fnun  5190  fconst5  5456  funfvima  5460  funsi  5521  fnpprod  5844  clos1conn  5880  trrd  5926  enprmaplem3  6079  nclenn  6250  ncslesuc  6268  nmembers1lem2  6270  nchoicelem17  6306  frecxp  6315  fnfrec  6321