Theorem expd 258

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

Hypothesis

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

Assertion

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

Proof of Theorem expd

Step	Hyp	Ref	Expression
1		exp3a.1	. . . 4 |- ( ph -> ( ( ps /\ ch ) -> th ) )
2	1	com12 30	. . 3 |- ( ( ps /\ ch ) -> ( ph -> th ) )
3	2	ex 115	. 2 |- ( ps -> ( ch -> ( ph -> th ) ) )
4	3	com3r 79	1 |- ( ph -> ( ps -> ( ch -> th ) ) )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  expdimp  259  pm3.3  261  syland  293  exp32  365  exp4c  368  exp4d  369  exp42  371  exp44  373  exp5c  376  impl  380  mpan2d  428  a2and  558  pm2.6dc  867  3impib  1225  exp5o  1250  biassdc  1437  exbir  1479  expcomd  1484  expdcom  1485  mopick  2156  ralrimivv  2611  mob2  2983  reuind  3008  difin  3441  reupick3  3489  suctr  4511  tfisi  4678  relop  4871  funcnvuni  5389  fnun  5428  mpteqb  5724  funfvima  5870  riotaeqimp  5978  poxp  6376  nnmass  6631  rex2dom  6969  supisoti  7173  axprecex  8063  ltnsym  8228  nn0lt2  9524  fzind  9558  fnn0ind  9559  btwnz  9562  lbzbi  9807  ledivge1le  9918  elfz0ubfz0  10317  elfzo0z  10380  fzofzim  10384  flqeqceilz  10535  leexp2r  10810  bernneq  10877  swrdswrdlem  11231  swrdswrd  11232  wrd2ind  11250  swrdccatin1  11252  swrdccatin2  11256  pfxccatin12lem3  11259  cau3lem  11620  climuni  11799  mulcn2  11818  dvdsabseq  12353  ndvdssub  12436  bezoutlemmain  12514  rplpwr  12543  algcvgblem  12566  euclemma  12663  insubm  13513  grpinveu  13566  srgmulgass  13947  basis2  14716  txcnp  14939  metcnp3  15179  gausslemma2dlem3  15736  bj-charfunr  16131