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  425  a2and  548  pm2.6dc  852  3impib  1191  exp5o  1216  biassdc  1385  exbir  1424  expcomd  1429  expdcom  1430  mopick  2092  ralrimivv  2547  mob2  2906  reuind  2931  difin  3359  reupick3  3407  suctr  4399  tfisi  4564  relop  4754  funcnvuni  5257  fnun  5294  mpteqb  5576  funfvima  5716  poxp  6200  nnmass  6455  supisoti  6975  axprecex  7821  ltnsym  7984  nn0lt2  9272  fzind  9306  fnn0ind  9307  btwnz  9310  lbzbi  9554  ledivge1le  9662  elfz0ubfz0  10060  elfzo0z  10119  fzofzim  10123  flqeqceilz  10253  leexp2r  10509  bernneq  10575  cau3lem  11056  climuni  11234  mulcn2  11253  dvdsabseq  11785  ndvdssub  11867  bezoutlemmain  11931  rplpwr  11960  algcvgblem  11981  euclemma  12078  basis2  12686  txcnp  12911  metcnp3  13151  bj-charfunr  13692