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  558  pm2.6dc  867  3impib  1225  exp5o  1250  biassdc  1437  exbir  1479  expcomd  1484  expdcom  1485  mopick  2156  ralrimivv  2611  mob2  2984  reuind  3009  difin  3442  reupick3  3490  suctr  4516  tfisi  4683  relop  4878  funcnvuni  5396  fnun  5435  mpteqb  5733  funfvima  5881  riotaeqimp  5991  poxp  6392  nnmass  6650  rex2dom  6991  supisoti  7200  axprecex  8090  ltnsym  8255  nn0lt2  9551  fzind  9585  fnn0ind  9586  btwnz  9589  lbzbi  9840  ledivge1le  9951  elfz0ubfz0  10350  elfzo0z  10413  fzofzim  10417  flqeqceilz  10570  leexp2r  10845  bernneq  10912  swrdswrdlem  11275  swrdswrd  11276  wrd2ind  11294  swrdccatin1  11296  swrdccatin2  11300  pfxccatin12lem3  11303  cau3lem  11665  climuni  11844  mulcn2  11863  dvdsabseq  12398  ndvdssub  12481  bezoutlemmain  12559  rplpwr  12588  algcvgblem  12611  euclemma  12708  insubm  13558  grpinveu  13611  srgmulgass  13992  basis2  14762  txcnp  14985  metcnp3  15225  gausslemma2dlem3  15782  wlkl1loop  16155  wlk1walkdom  16156  uspgr2wlkeq  16162  bj-charfunr  16341