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  864  3impib  1204  exp5o  1229  biassdc  1415  exbir  1457  expcomd  1462  expdcom  1463  mopick  2133  ralrimivv  2588  mob2  2957  reuind  2982  difin  3414  reupick3  3462  suctr  4476  tfisi  4643  relop  4836  funcnvuni  5352  fnun  5391  mpteqb  5683  funfvima  5829  poxp  6331  nnmass  6586  rex2dom  6924  supisoti  7127  axprecex  8013  ltnsym  8178  nn0lt2  9474  fzind  9508  fnn0ind  9509  btwnz  9512  lbzbi  9757  ledivge1le  9868  elfz0ubfz0  10267  elfzo0z  10330  fzofzim  10334  flqeqceilz  10485  leexp2r  10760  bernneq  10827  swrdswrdlem  11180  swrdswrd  11181  wrd2ind  11199  cau3lem  11500  climuni  11679  mulcn2  11698  dvdsabseq  12233  ndvdssub  12316  bezoutlemmain  12394  rplpwr  12423  algcvgblem  12446  euclemma  12543  insubm  13392  grpinveu  13445  srgmulgass  13826  basis2  14595  txcnp  14818  metcnp3  15058  gausslemma2dlem3  15615  bj-charfunr  15884