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  2940  reuind  2965  difin  3396  reupick3  3444  suctr  4452  tfisi  4619  relop  4812  funcnvuni  5323  fnun  5360  mpteqb  5648  funfvima  5790  poxp  6285  nnmass  6540  supisoti  7069  axprecex  7940  ltnsym  8105  nn0lt2  9398  fzind  9432  fnn0ind  9433  btwnz  9436  lbzbi  9681  ledivge1le  9792  elfz0ubfz0  10191  elfzo0z  10251  fzofzim  10255  flqeqceilz  10389  leexp2r  10664  bernneq  10731  cau3lem  11258  climuni  11436  mulcn2  11455  dvdsabseq  11989  ndvdssub  12071  bezoutlemmain  12135  rplpwr  12164  algcvgblem  12187  euclemma  12284  insubm  13057  grpinveu  13110  srgmulgass  13485  basis2  14216  txcnp  14439  metcnp3  14679  gausslemma2dlem3  15179  bj-charfunr  15302