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  11367  climuni  11546  mulcn2  11565  dvdsabseq  12100  ndvdssub  12183  bezoutlemmain  12261  rplpwr  12290  algcvgblem  12313  euclemma  12410  insubm  13259  grpinveu  13312  srgmulgass  13693  basis2  14462  txcnp  14685  metcnp3  14925  gausslemma2dlem3  15482  bj-charfunr  15679