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  432  a2and  564  pm2.6dc  874  3impib  1232  exp5o  1257  biassdc  1444  exbir  1486  expcomd  1491  expdcom  1492  mopick  2165  ralrimivv  2631  mob2  3006  reuind  3031  difin  3468  reupick3  3518  suctr  4561  tfisi  4729  relop  4925  funcnvuni  5445  fnun  5484  mpteqb  5790  funfvima  5940  riotaeqimp  6053  poxp  6458  nnmass  6750  rex2dom  7100  supisoti  7340  axprecex  8237  ltnsym  8401  nn0lt2  9706  fzind  9740  fnn0ind  9741  btwnz  9744  lbzbi  9995  ledivge1le  10106  elfz0ubfz0  10510  elfzo0z  10574  fzofzim  10578  flqeqceilz  10733  leexp2r  11008  bernneq  11076  swrdswrdlem  11454  swrdswrd  11455  wrd2ind  11473  swrdccatin1  11475  swrdccatin2  11479  pfxccatin12lem3  11482  cau3lem  11858  climuni  12037  mulcn2  12056  dvdsabseq  12592  ndvdssub  12675  bezoutlemmain  12753  rplpwr  12782  algcvgblem  12805  euclemma  12902  insubm  13769  grpinveu  13820  srgmulgass  14267  basis2  15072  txcnp  15295  metcnp3  15535  gausslemma2dlem3  16096  wlkl1loop  16513  wlk1walkdom  16514  uspgr2wlkeq  16520  eupth2lem3lem6fi  16626  lealltlt2  16666  bj-charfunr  16750