Theorem impexp 446

Description: Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)

Assertion

Ref	Expression
impexp

Proof of Theorem impexp

Step	Hyp	Ref	Expression
1		pm3.3 444	. 2
2		pm3.31 445	. 2
3	1, 2	impbii 188	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369

This theorem is referenced by:  pm4.14  578  nan  580  pm4.87  584  imp4a  589  exp4a  606  imdistan  689  pm5.3  711  pm5.6  912  2sb6  2188  2eu6OLD  2384  r2allem  2832  r2alfOLD  2834  r3al  2837  r3alOLD  2895  r19.23t  2935  ceqsralt  3133  ralrab  3261  ralrab2  3265  euind  3286  reu2  3287  reu3  3289  rmo4  3292  reuind  3303  2reu5lem3  3307  rmo2  3427  rmo3  3429  ralss  3565  rabss  3576  raldifb  3643  raldifsni  4160  unissb  4281  elintrab  4298  ssintrab  4310  dftr5  4548  axrep5  4568  reusv2lem4  4656  reusv2  4658  reusv3  4660  raliunxp  5147  fununi  5659  fvn0ssdmfun  6022  dff13  6166  ordunisuc2  6679  dfom2  6702  dfsmo2  7037  qliftfun  7415  dfsup2  7922  wemapsolem  7996  iscard2  8378  acnnum  8454  aceq1  8519  dfac9  8537  dfacacn  8542  axgroth6  9227  sstskm  9241  infm3  10527  prime  10968  raluz  11158  raluz2  11159  nnwos  11178  ralrp  11267  facwordi  12367  rexuzre  13185  limsupgle  13300  ello12  13339  elo12  13350  lo1resb  13387  rlimresb  13388  o1resb  13389  modfsummod  13608  isprm2  14225  isprm4  14227  acsfn2  15060  pgpfac1  17131  isirred2  17350  isdomn2  17948  coe1fzgsumd  18344  evl1gsumd  18393  islindf4  18873  ist1-2  19848  isnrm2  19859  dfcon2  19920  1stccn  19964  iskgen3  20050  hausdiag  20146  cnflf  20503  txflf  20507  cnfcf  20543  metcnp  21044  caucfil  21722  ovolgelb  21891  ismbl  21937  dyadmbllem  22008  itg2leub  22141  ellimc3  22283  mdegleb  22464  jensen  23318  dchrelbas2  23512  dchrelbas3  23513  nmoubi  25687  nmobndseqi  25694  nmobndseqiOLD  25695  h1dei  26468  nmopub  26827  nmfnleub  26844  mdsl1i  27240  mdsl2i  27241  elat2  27259  moel  27382  rmo3f  27394  rmo4fOLD  27395  eulerpartlemgvv  28315  climuzcnv  29037  axextprim  29073  biimpexp  29093  dfpo2  29184  dfon2lem8  29222  predreseq  29259  dffun10  29564  wl-2sb6d  30008  filnetlem4  30199  dford4  30971  fnwe2lem2  30997  isdomn3  31164  isprm7  31192  pm11.62  31300  2sbc6g  31322  2rexsb  32175  2rexrsb  32176  rmoanim  32184  rabsssn  32920  snlindsntor  33072  expcomdg  33269  impexpd  33283  dfvd2  33356  dfvd3  33368  bnj115  33778  bnj1109  33845  bnj1533  33910  bnj580  33971  bnj864  33980  bnj865  33981  bnj1049  34030  bnj1090  34035  bnj1093  34036  bnj1133  34045  bnj1171  34056  bj-axrep5  34378  isat3  35032  isltrn2N  35844  cdlemefrs29bpre0  36122  cdleme32fva  36163  bj-ifidg  37707  cotr2g  37786  dfhe3  37799

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