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  2123  ralrimivv  2578  mob2  2944  reuind  2969  difin  3401  reupick3  3449  suctr  4457  tfisi  4624  relop  4817  funcnvuni  5328  fnun  5367  mpteqb  5655  funfvima  5797  poxp  6299  nnmass  6554  supisoti  7085  axprecex  7964  ltnsym  8129  nn0lt2  9424  fzind  9458  fnn0ind  9459  btwnz  9462  lbzbi  9707  ledivge1le  9818  elfz0ubfz0  10217  elfzo0z  10277  fzofzim  10281  flqeqceilz  10427  leexp2r  10702  bernneq  10769  cau3lem  11296  climuni  11475  mulcn2  11494  dvdsabseq  12029  ndvdssub  12112  bezoutlemmain  12190  rplpwr  12219  algcvgblem  12242  euclemma  12339  insubm  13187  grpinveu  13240  srgmulgass  13621  basis2  14368  txcnp  14591  metcnp3  14831  gausslemma2dlem3  15388  bj-charfunr  15540