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  2705  mob2  3016  reuind  3039  reupick3  3540  pwadjoin  4119  opkthg  4131  nndisjeq  4429  ssfin  4470  ncfinraise  4481  sfin112  4529  sfintfin  4532  vfinspss  4551  phi11lem1  4595  funcnvuni  5161  fnun  5189  fconst5  5455  funfvima  5459  funsi  5520  fnpprod  5843  clos1conn  5879  trrd  5925  enprmaplem3  6078  nclenn  6249  ncslesuc  6267  nmembers1lem2  6269  nchoicelem17  6305  frecxp  6314  fnfrec  6320