Theorem expdimp 435

Description: A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.)

Hypothesis

Ref	Expression
exp3a.1	|- ( ph -> ( ( ps /\ ch ) -> th ) )

Assertion

Ref	Expression
expdimp	|- ( ( ph /\ ps ) -> ( ch -> th ) )

Proof of Theorem expdimp

Step	Hyp	Ref	Expression
1		exp3a.1	. . 3 |- ( ph -> ( ( ps /\ ch ) -> th ) )
2	1	expd 434	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp 427	1 |- ( ( ph /\ ps ) -> ( ch -> th ) )

Syntax hints:   -> wi 4   /\ wa 367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 369

This theorem is referenced by:  rexlimdvv  2902  ralcom2  2972  reu6  3238  ssexnelpss  3836  wereu2  4820  ordtr3  5455  oneqmini  5461  suppssrOLD  5999  fun11iun  6744  poxp  6896  suppssr  6934  smoel  7064  omabs  7333  omsmo  7340  iiner  7420  fodomr  7706  fisseneq  7766  suplub2  7954  supnub  7955  inf3lem6  8083  cfcoflem  8684  coftr  8685  zorn2lem7  8914  alephreg  8989  inar1  9183  gruen  9220  letr  9709  lbzbi  11215  xrletr  11414  xmullem  11509  supxrun  11560  ssfzoulel  11943  ssfzo12bi  11944  hashbnd  12458  brfi1uzind  12581  cau3lem  13336  summo  13688  mertenslem2  13846  prodmolem2  13894  alzdvds  14245  nn0seqcvgd  14408  prmn2uzge3  14446  divgcdodd  14469  prmpwdvds  14631  catpropd  15322  pltnle  15920  pltval3  15921  pltletr  15925  tsrlemax  16174  frgpnabllem1  17201  cyggexb  17225  abvn0b  18271  isphld  18987  indistopon  19794  restntr  19976  cnprest  20083  lmss  20092  lmmo  20174  2ndcdisj  20249  txlm  20441  flftg  20789  bndth  21750  iscmet3  22024  bcthlem5  22059  ovolicc2lem4  22223  ellimc3  22575  lhop1  22707  ulmcaulem  23081  ulmcau  23082  ulmcn  23086  xrlimcnp  23624  ax5seglem4  24652  axcontlem2  24685  axcontlem4  24687  clwlkisclwwlklem2a  25202  rusgrasn  25362  frgrawopreglem5  25465  extwwlkfablem2  25495  gxadd  25691  gxmul  25694  nmcvcn  26019  htthlem  26248  atcvat3i  27728  sumdmdlem2  27751  ifeqeqx  27840  bnj23  29098  bnj849  29310  funbreq  29984  sltasym  30132  cgrdegen  30342  lineext  30414  btwnconn1lem7  30431  btwnconn1lem14  30438  waj-ax  30646  lukshef-ax2  30647  relowlssretop  31280  fin2solem  31411  unirep  31485  seqpo  31522  ssbnd  31566  intidl  31708  prnc  31746  prtlem15  31898  lshpkrlem6  32133  atlatmstc  32337  cvrat3  32459  ps-2  32495  2lplnj  32637  paddasslem5  32841  dochkrshp4  34409  isnacs3  35004  lcmdvds  36062  pm14.24  36187  rexlim2d  36999  iccpartigtl  37690  icceuelpartlem  37702  rngcinv  38300  rngcinvALTV  38312  ringcinv  38351  ringcinvALTV  38375  lindslinindsimp1  38569  lindslinindsimp2  38575  nno  38648  digexp  38738  aacllem  38860