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  862  3impib  1201  exp5o  1226  biassdc  1395  exbir  1436  expcomd  1441  expdcom  1442  mopick  2104  ralrimivv  2558  mob2  2919  reuind  2944  difin  3374  reupick3  3422  suctr  4423  tfisi  4588  relop  4779  funcnvuni  5287  fnun  5324  mpteqb  5609  funfvima  5751  poxp  6236  nnmass  6491  supisoti  7012  axprecex  7882  ltnsym  8046  nn0lt2  9337  fzind  9371  fnn0ind  9372  btwnz  9375  lbzbi  9619  ledivge1le  9729  elfz0ubfz0  10128  elfzo0z  10187  fzofzim  10191  flqeqceilz  10321  leexp2r  10577  bernneq  10644  cau3lem  11126  climuni  11304  mulcn2  11323  dvdsabseq  11856  ndvdssub  11938  bezoutlemmain  12002  rplpwr  12031  algcvgblem  12052  euclemma  12149  insubm  12879  grpinveu  12918  srgmulgass  13183  basis2  13709  txcnp  13932  metcnp3  14172  bj-charfunr  14723