Theorem expd 256

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 114	. 2 |- ( ps -> ( ch -> ( ph -> th ) ) )
4	3	com3r 79	1 |- ( ph -> ( ps -> ( ch -> th ) ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  expdimp  257  pm3.3  259  syland  291  exp32  363  exp4c  366  exp4d  367  exp42  369  exp44  371  exp5c  374  impl  378  mpan2d  426  a2and  553  pm2.6dc  857  3impib  1196  exp5o  1221  biassdc  1390  exbir  1429  expcomd  1434  expdcom  1435  mopick  2097  ralrimivv  2551  mob2  2910  reuind  2935  difin  3364  reupick3  3412  suctr  4406  tfisi  4571  relop  4761  funcnvuni  5267  fnun  5304  mpteqb  5586  funfvima  5727  poxp  6211  nnmass  6466  supisoti  6987  axprecex  7842  ltnsym  8005  nn0lt2  9293  fzind  9327  fnn0ind  9328  btwnz  9331  lbzbi  9575  ledivge1le  9683  elfz0ubfz0  10081  elfzo0z  10140  fzofzim  10144  flqeqceilz  10274  leexp2r  10530  bernneq  10596  cau3lem  11078  climuni  11256  mulcn2  11275  dvdsabseq  11807  ndvdssub  11889  bezoutlemmain  11953  rplpwr  11982  algcvgblem  12003  euclemma  12100  insubm  12703  grpinveu  12741  basis2  12840  txcnp  13065  metcnp3  13305  bj-charfunr  13845