Theorem expd 255

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-1 5  ax-2 6  ax-mp 7  ax-ia3 107

This theorem is referenced by:  expdimp  256  pm3.3  258  syland  288  exp32  358  exp4c  361  exp4d  362  exp42  364  exp44  366  exp5c  369  impl  373  mpan2d  420  a2and  526  pm2.6dc  800  3impib  1144  exp5o  1169  biassdc  1338  exbir  1377  expcomd  1382  expdcom  1383  mopick  2033  ralrimivv  2466  mob2  2809  reuind  2834  difin  3252  reupick3  3300  suctr  4272  tfisi  4430  relop  4617  funcnvuni  5117  fnun  5154  mpteqb  5429  funfvima  5565  poxp  6035  nnmass  6288  supisoti  6785  axprecex  7512  ltnsym  7668  nn0lt2  8926  fzind  8960  fnn0ind  8961  btwnz  8964  lbzbi  9200  ledivge1le  9302  elfz0ubfz0  9685  elfzo0z  9744  fzofzim  9748  flqeqceilz  9874  leexp2r  10124  bernneq  10189  cau3lem  10662  climuni  10836  mulcn2  10855  dvdsabseq  11275  ndvdssub  11357  bezoutlemmain  11414  rplpwr  11443  algcvgblem  11458  euclemma  11552  basis2  11898  metcnp3  12293