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  560  pm2.6dc  869  3impib  1227  exp5o  1252  biassdc  1439  exbir  1481  expcomd  1486  expdcom  1487  mopick  2158  ralrimivv  2613  mob2  2986  reuind  3011  difin  3444  reupick3  3492  suctr  4518  tfisi  4685  relop  4880  funcnvuni  5399  fnun  5438  mpteqb  5737  funfvima  5885  riotaeqimp  5995  poxp  6396  nnmass  6654  rex2dom  6995  supisoti  7208  axprecex  8099  ltnsym  8264  nn0lt2  9560  fzind  9594  fnn0ind  9595  btwnz  9598  lbzbi  9849  ledivge1le  9960  elfz0ubfz0  10359  elfzo0z  10422  fzofzim  10426  flqeqceilz  10579  leexp2r  10854  bernneq  10921  swrdswrdlem  11284  swrdswrd  11285  wrd2ind  11303  swrdccatin1  11305  swrdccatin2  11309  pfxccatin12lem3  11312  cau3lem  11674  climuni  11853  mulcn2  11872  dvdsabseq  12407  ndvdssub  12490  bezoutlemmain  12568  rplpwr  12597  algcvgblem  12620  euclemma  12717  insubm  13567  grpinveu  13620  srgmulgass  14001  basis2  14771  txcnp  14994  metcnp3  15234  gausslemma2dlem3  15791  wlkl1loop  16208  wlk1walkdom  16209  uspgr2wlkeq  16215  bj-charfunr  16405