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  863  3impib  1203  exp5o  1228  biassdc  1406  exbir  1447  expcomd  1452  expdcom  1453  mopick  2120  ralrimivv  2575  mob2  2941  reuind  2966  difin  3397  reupick3  3445  suctr  4453  tfisi  4620  relop  4813  funcnvuni  5324  fnun  5361  mpteqb  5649  funfvima  5791  poxp  6287  nnmass  6542  supisoti  7071  axprecex  7942  ltnsym  8107  nn0lt2  9401  fzind  9435  fnn0ind  9436  btwnz  9439  lbzbi  9684  ledivge1le  9795  elfz0ubfz0  10194  elfzo0z  10254  fzofzim  10258  flqeqceilz  10392  leexp2r  10667  bernneq  10734  cau3lem  11261  climuni  11439  mulcn2  11458  dvdsabseq  11992  ndvdssub  12074  bezoutlemmain  12138  rplpwr  12167  algcvgblem  12190  euclemma  12287  insubm  13060  grpinveu  13113  srgmulgass  13488  basis2  14227  txcnp  14450  metcnp3  14690  gausslemma2dlem3  15220  bj-charfunr  15372