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  2983  reuind  3008  difin  3441  reupick3  3489  suctr  4512  tfisi  4679  relop  4872  funcnvuni  5390  fnun  5429  mpteqb  5727  funfvima  5875  riotaeqimp  5985  poxp  6384  nnmass  6641  rex2dom  6979  supisoti  7188  axprecex  8078  ltnsym  8243  nn0lt2  9539  fzind  9573  fnn0ind  9574  btwnz  9577  lbzbi  9823  ledivge1le  9934  elfz0ubfz0  10333  elfzo0z  10396  fzofzim  10400  flqeqceilz  10552  leexp2r  10827  bernneq  10894  swrdswrdlem  11251  swrdswrd  11252  wrd2ind  11270  swrdccatin1  11272  swrdccatin2  11276  pfxccatin12lem3  11279  cau3lem  11640  climuni  11819  mulcn2  11838  dvdsabseq  12373  ndvdssub  12456  bezoutlemmain  12534  rplpwr  12563  algcvgblem  12586  euclemma  12683  insubm  13533  grpinveu  13586  srgmulgass  13967  basis2  14737  txcnp  14960  metcnp3  15200  gausslemma2dlem3  15757  wlkl1loop  16099  wlk1walkdom  16100  uspgr2wlkeq  16106  bj-charfunr  16228