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  2161  ralrimivv  2625  mob2  3000  reuind  3025  difin  3462  reupick3  3510  suctr  4547  tfisi  4714  relop  4910  funcnvuni  5430  fnun  5469  mpteqb  5773  funfvima  5923  riotaeqimp  6036  poxp  6441  nnmass  6733  rex2dom  7076  supisoti  7314  axprecex  8211  ltnsym  8375  nn0lt2  9677  fzind  9711  fnn0ind  9712  btwnz  9715  lbzbi  9966  ledivge1le  10077  elfz0ubfz0  10481  elfzo0z  10545  fzofzim  10549  flqeqceilz  10704  leexp2r  10979  bernneq  11047  swrdswrdlem  11421  swrdswrd  11422  wrd2ind  11440  swrdccatin1  11442  swrdccatin2  11446  pfxccatin12lem3  11449  cau3lem  11824  climuni  12003  mulcn2  12022  dvdsabseq  12558  ndvdssub  12641  bezoutlemmain  12719  rplpwr  12748  algcvgblem  12771  euclemma  12868  insubm  13740  grpinveu  13793  srgmulgass  14232  basis2  15039  txcnp  15262  metcnp3  15502  gausslemma2dlem3  16062  wlkl1loop  16479  wlk1walkdom  16480  uspgr2wlkeq  16486  eupth2lem3lem6fi  16592  bj-charfunr  16706