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  560  pm2.6dc  869  3impib  1227  exp5o  1252  biassdc  1439  exbir  1481  expcomd  1486  expdcom  1487  mopick  2158  ralrimivv  2613  mob2  2986  reuind  3011  difin  3444  reupick3  3492  suctr  4518  tfisi  4685  relop  4880  funcnvuni  5399  fnun  5438  mpteqb  5737  funfvima  5886  riotaeqimp  5996  poxp  6397  nnmass  6655  rex2dom  6996  supisoti  7209  axprecex  8100  ltnsym  8265  nn0lt2  9561  fzind  9595  fnn0ind  9596  btwnz  9599  lbzbi  9850  ledivge1le  9961  elfz0ubfz0  10360  elfzo0z  10424  fzofzim  10428  flqeqceilz  10581  leexp2r  10856  bernneq  10923  swrdswrdlem  11289  swrdswrd  11290  wrd2ind  11308  swrdccatin1  11310  swrdccatin2  11314  pfxccatin12lem3  11317  cau3lem  11692  climuni  11871  mulcn2  11890  dvdsabseq  12426  ndvdssub  12509  bezoutlemmain  12587  rplpwr  12616  algcvgblem  12639  euclemma  12736  insubm  13586  grpinveu  13639  srgmulgass  14021  basis2  14791  txcnp  15014  metcnp3  15254  gausslemma2dlem3  15811  wlkl1loop  16228  wlk1walkdom  16229  uspgr2wlkeq  16235  eupth2lem3lem6fi  16341  bj-charfunr  16456