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  2158  ralrimivv  2614  mob2  2987  reuind  3012  difin  3446  reupick3  3494  suctr  4524  tfisi  4691  relop  4886  funcnvuni  5406  fnun  5445  mpteqb  5746  funfvima  5896  riotaeqimp  6006  poxp  6406  nnmass  6698  rex2dom  7039  supisoti  7252  axprecex  8143  ltnsym  8307  nn0lt2  9605  fzind  9639  fnn0ind  9640  btwnz  9643  lbzbi  9894  ledivge1le  10005  elfz0ubfz0  10405  elfzo0z  10469  fzofzim  10473  flqeqceilz  10626  leexp2r  10901  bernneq  10968  swrdswrdlem  11334  swrdswrd  11335  wrd2ind  11353  swrdccatin1  11355  swrdccatin2  11359  pfxccatin12lem3  11362  cau3lem  11737  climuni  11916  mulcn2  11935  dvdsabseq  12471  ndvdssub  12554  bezoutlemmain  12632  rplpwr  12661  algcvgblem  12684  euclemma  12781  insubm  13631  grpinveu  13684  srgmulgass  14066  basis2  14842  txcnp  15065  metcnp3  15305  gausslemma2dlem3  15865  wlkl1loop  16282  wlk1walkdom  16283  uspgr2wlkeq  16289  eupth2lem3lem6fi  16395  bj-charfunr  16509