Theorem expdimp 437

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

Hypothesis

Ref	Expression
exp3a.1

Assertion

Ref	Expression
expdimp

Proof of Theorem expdimp

Step	Hyp	Ref	Expression
1		exp3a.1	. . 3
2	1	expd 436	. 2
3	2	imp 429	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  rexlimdvv  2955  ralcom2  3022  reu6  3288  ssexnelpss  3892  wereu2  4881  ordtr3  4928  oneqmini  4934  suppssrOLD  6021  fun11iun  6760  poxp  6912  suppssr  6950  smoel  7050  omabs  7315  omsmo  7322  iiner  7402  fodomr  7688  fisseneq  7751  suplub2  7941  supnub  7942  inf3lem6  8071  cfcoflem  8673  coftr  8674  zorn2lem7  8903  alephreg  8978  inar1  9174  gruen  9211  letr  9699  lbzbi  11199  xrletr  11390  xmullem  11485  supxrun  11536  ssfzoulel  11906  ssfzo12bi  11907  hashbnd  12411  brfi1uzind  12532  cau3lem  13187  summo  13539  mertenslem2  13694  prodmolem2  13742  alzdvds  14036  nn0seqcvgd  14199  prmn2uzge3  14237  divgcdodd  14260  prmpwdvds  14422  catpropd  15104  pltnle  15596  pltval3  15597  pltletr  15601  tsrlemax  15850  frgpnabllem1  16877  cyggexb  16901  abvn0b  17951  isphld  18689  indistopon  19502  restntr  19683  cnprest  19790  lmss  19799  lmmo  19881  2ndcdisj  19957  txlm  20149  flftg  20497  bndth  21458  iscmet3  21732  bcthlem5  21767  ovolicc2lem4  21931  ellimc3  22283  lhop1  22415  ulmcaulem  22789  ulmcau  22790  ulmcn  22794  xrlimcnp  23298  ax5seglem4  24235  axcontlem2  24268  axcontlem4  24270  clwlkisclwwlklem2a  24785  rusgrasn  24945  frgrawopreglem5  25048  extwwlkfablem2  25078  gxadd  25277  gxmul  25280  nmcvcn  25605  htthlem  25834  atcvat3i  27315  sumdmdlem2  27338  ifeqeqx  27419  funbreq  29201  sltasym  29432  cgrdegen  29654  lineext  29726  btwnconn1lem7  29743  btwnconn1lem14  29750  waj-ax  29879  lukshef-ax2  29880  fin2solem  30039  unirep  30203  seqpo  30240  ssbnd  30284  intidl  30426  prnc  30464  prtlem15  30616  isnacs3  30642  lcmdvds  31214  pm14.24  31339  rexlim2d  31631  rngcinv  32789  rngcinvOLD  32801  ringcinv  32840  ringcinvOLD  32864  lindslinindsimp1  33058  lindslinindsimp2  33064  aacllem  33216  bnj23  33771  bnj849  33983  lshpkrlem6  34840  atlatmstc  35044  cvrat3  35166  ps-2  35202  2lplnj  35344  paddasslem5  35548  dochkrshp4  37116

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 371