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  1414  exbir  1455  expcomd  1460  expdcom  1461  mopick  2131  ralrimivv  2586  mob2  2952  reuind  2977  difin  3409  reupick3  3457  suctr  4467  tfisi  4634  relop  4827  funcnvuni  5342  fnun  5381  mpteqb  5669  funfvima  5815  poxp  6317  nnmass  6572  rex2dom  6909  supisoti  7111  axprecex  7992  ltnsym  8157  nn0lt2  9453  fzind  9487  fnn0ind  9488  btwnz  9491  lbzbi  9736  ledivge1le  9847  elfz0ubfz0  10246  elfzo0z  10306  fzofzim  10310  flqeqceilz  10461  leexp2r  10736  bernneq  10803  cau3lem  11396  climuni  11575  mulcn2  11594  dvdsabseq  12129  ndvdssub  12212  bezoutlemmain  12290  rplpwr  12319  algcvgblem  12342  euclemma  12439  insubm  13288  grpinveu  13341  srgmulgass  13722  basis2  14491  txcnp  14714  metcnp3  14954  gausslemma2dlem3  15511  bj-charfunr  15708