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  870  3impib  1228  exp5o  1253  biassdc  1440  exbir  1482  expcomd  1487  expdcom  1488  mopick  2159  ralrimivv  2623  mob2  2997  reuind  3022  difin  3458  reupick3  3506  suctr  4542  tfisi  4709  relop  4905  funcnvuni  5425  fnun  5464  mpteqb  5768  funfvima  5918  riotaeqimp  6028  poxp  6428  nnmass  6720  rex2dom  7063  supisoti  7301  axprecex  8195  ltnsym  8359  nn0lt2  9659  fzind  9693  fnn0ind  9694  btwnz  9697  lbzbi  9948  ledivge1le  10059  elfz0ubfz0  10459  elfzo0z  10523  fzofzim  10527  flqeqceilz  10680  leexp2r  10955  bernneq  11022  swrdswrdlem  11396  swrdswrd  11397  wrd2ind  11415  swrdccatin1  11417  swrdccatin2  11421  pfxccatin12lem3  11424  cau3lem  11799  climuni  11978  mulcn2  11997  dvdsabseq  12533  ndvdssub  12616  bezoutlemmain  12694  rplpwr  12723  algcvgblem  12746  euclemma  12843  insubm  13698  grpinveu  13751  srgmulgass  14133  basis2  14913  txcnp  15136  metcnp3  15376  gausslemma2dlem3  15936  wlkl1loop  16353  wlk1walkdom  16354  uspgr2wlkeq  16360  eupth2lem3lem6fi  16466  bj-charfunr  16580