ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ex Structured version   Unicode version

Theorem ex 108
Description: Exportation inference. (This theorem used to be labeled "exp" but was changed to "ex" so as not to conflict with the math token "exp", per the June 2006 Metamath spec change.) (Contributed by NM, 5-Aug-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
Hypothesis
Ref Expression
exp.1
Assertion
Ref Expression
ex

Proof of Theorem ex
StepHypRef Expression
1 ax-ia3 101 . 2
2 exp.1 . 2
31, 2syl6 29 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  expcom  109  bi3  112  pm3.2  126  expd  245  impancom  247  expimpd  345  exp31  346  exp32  347  exp4b  349  exp41  352  exp43  354  exp53  359  impr  361  simplbi2  367  anidms  377  syl2anc  391  pm5.74da  417  imdistanda  422  pm5.32da  425  impbida  528  anim12dan  532  pm2.01da  564  pm2.65da  586  mtand  590  pm5.21im  611  jao  671  jaoian  708  jaodan  709  impidc  754  pm2.5dc  762  con1bidc  767  con2bidc  768  con1bdc  771  pm5.18dc  776  dfandc  777  pm4.63dc  779  dcim  783  pm4.54dc  804  pm5.21nd  824  dcan  841  dcor  842  annimdc  844  pm4.55dc  845  pm3.11dc  863  pm3.12dc  864  prlem1  879  pm3.2an3  1082  3jcad  1084  3impia  1100  3an1rs  1115  3exp1  1119  3exp2  1121  exp520  1124  syl3anl2  1183  3jaoian  1199  3jaodan  1200  mp3anl1  1225  mp3anl2  1226  mp3anl3  1227  inegd  1262  xor3dc  1275  pm5.15dc  1277  xor2dc  1278  xornbidc  1279  xordc  1280  nbbndc  1282  biassdc  1283  dfbi3dc  1285  pm5.24dc  1286  alanimi  1345  equsexd  1614  sbequ1  1648  sbiedv  1669  ax11v2  1698  equs5or  1708  sbequi  1717  exlimdd  1749  exlimddv  1775  cbvaldva  1800  cbvexdva  1801  nfsbxyt  1816  sbcomxyyz  1843  nfsb4t  1887  eupickbi  1979  moexexdc  1981  euexex  1982  2euswapdc  1988  dvelimdc  2194  nebidc  2279  rgen2a  2369  ralimiaa  2377  ralimdaa  2380  ralrimiva  2386  ralrimdva  2393  ralrimivva  2395  ralrimdvv  2397  ralrimdvva  2398  reximdva  2415  rexlimiva  2422  rexlimdva  2427  rexlimdvva  2434  r19.29vva  2450  2gencl  2581  vtocldf  2599  spcimdv  2631  spcimedv  2633  rspct  2643  eqvinc  2661  eqvincg  2662  ceqex  2665  reu6  2724  eqreu  2727  sbciedf  2792  rmob  2844  csbiebt  2880  csbiedf  2881  reupick  3215  reximdva0m  3230  ssn0  3253  rgenm  3317  preqr1g  3528  prel12  3533  dfnfc2  3589  intssunim  3628  intab  3635  iineq2d  3668  ssiun2  3691  mpteq2da  3837  trintssm  3861  copsexg  3972  copsex2t  3973  sess1  4059  sess2  4060  tron  4085  onelss  4090  onintss  4093  reusv1  4156  reusv3  4158  rabxfrd  4167  iunpw  4177  ssorduni  4179  ordsson  4184  ordsucg  4194  onsucelsucexmidlem  4214  elirr  4224  en2lp  4232  ordsuc  4241  ordpwsucss  4243  tfisi  4253  sosng  4356  2optocl  4360  relop  4429  xpid11m  4500  releldmb  4514  relelrnb  4515  elrnmptg  4529  elreimasng  4634  relbrcnvg  4647  trin2  4659  ssxpbm  4699  ssxp1  4700  ssxp2  4701  elxp4  4751  elxp5  4752  relresfld  4790  relcoi1  4792  iotaval  4821  iotass  4827  funmo  4860  imadif  4922  imain  4924  2elresin  4953  feu  5015  fcnvres  5016  f1oun  5089  f1oprg  5111  relfvssunirn  5134  funbrfv  5155  funbrfv2b  5161  dffn5im  5162  dfimafn  5165  funimass4  5167  ssimaex  5177  fvmptssdm  5198  fvmptf  5206  fvimacnv  5225  funimass3  5226  elpreima  5229  elrnrexdm  5249  eldmrexrn  5251  dffo4  5258  dffo5  5259  fmpt  5262  ffvresb  5271  fmptco  5273  fsn  5278  funfvima  5333  funfvima2  5334  f1mpt  5353  f1imass  5356  f1ocnvfvrneq  5365  foeqcnvco  5373  f1eqcocnv  5374  fliftfun  5379  fliftf  5382  isopolem  5404  isosolem  5406  eusvobj2  5441  acexmidlemab  5449  oprabid  5480  ovidi  5561  ovg  5581  suppssfv  5650  suppssov1  5651  funrnex  5683  f1dmex  5685  oprabexd  5696  fo2ndresm  5731  op1steq  5747  dfoprab3  5759  fo2ndf  5790  f1o2ndf1  5791  poxp  5794  isprmpt2  5799  reldmtpos  5809  rntpos  5813  tposf2  5824  tposf12  5825  issmo2  5845  smores  5848  smoiso  5858  tfrlem9  5876  tfrlemibacc  5881  tfrlemibfn  5883  tfrlemi14d  5888  tfrexlem  5889  rdgivallem  5908  frecsuclem3  5929  frecrdg  5931  freccl  5932  oawordi  5988  nnmcom  6007  nnsucelsuc  6009  nntri3or  6011  nntri1  6013  nnaordi  6017  nnmord  6026  nnaordex  6036  nnm00  6038  ertr  6057  erex  6066  iserd  6068  iinerm  6114  erinxp  6116  qsel  6119  qliftfun  6124  qliftfund  6125  2ecoptocl  6130  brecop  6132  dom2lem  6188  fundmen  6222  unen  6229  enm  6230  xpdom2  6241  fopwdom  6246  mulcanpig  6319  nlt1pig  6325  addcmpblnq  6351  ltsonq  6382  ltexnqq  6391  prarloclemarch2  6402  enq0tr  6416  addcmpblnq0  6425  addnq0mo  6429  mulnq0mo  6430  prcdnql  6466  prcunqu  6467  prarloclemlo  6476  prarloclem3step  6478  prarloclem3  6479  genpdflem  6489  genpelvl  6494  genpelvu  6495  genpcdl  6501  genpcuu  6502  genprndl  6503  genprndu  6504  genpdisj  6505  addnqprllem  6509  addnqprulem  6510  addlocprlemeq  6515  addlocprlemgt  6516  nqprloc  6527  nqprl  6532  addnqprlemrl  6537  addnqprlemru  6538  addnqprlemfl  6539  addnqprlemfu  6540  prmuloc  6546  prmuloc2  6547  mullocpr  6551  distrlem4prl  6559  distrlem4pru  6560  ltprordil  6564  1idprl  6565  1idpru  6566  ltpopr  6568  ltsopr  6569  ltaddpr  6570  ltexprlemm  6573  ltexprlemlol  6575  ltexprlemupu  6577  ltexprlemdisj  6579  ltexprlemloc  6580  ltexprlemrl  6583  ltexprlemru  6585  addcanprleml  6587  addcanprlemu  6588  addcanprg  6589  ltaprg  6591  recexprlemlol  6597  recexprlemdisj  6601  recexprlemloc  6602  recexprlem1ssl  6604  recexprlem1ssu  6605  aptiprleml  6610  aptiprlemu  6611  ltmprr  6613  archpr  6614  cauappcvgprlemm  6616  cauappcvgprlemopl  6617  cauappcvgprlemlol  6618  cauappcvgprlemopu  6619  cauappcvgprlemrnd  6621  cauappcvgprlemloc  6623  cauappcvgprlemladdfu  6625  cauappcvgprlemladdfl  6626  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  mulcmpblnrlemg  6648  addsrmo  6651  mulsrmo  6652  ltsrprg  6655  pitonn  6724  lelttr  6883  ltletr  6884  readdcan  6930  cnegexlem1  6963  cnegexlem2  6964  add20  7244  recexre  7342  inelr  7348  rimul  7349  apreap  7351  ltmul1  7356  cru  7366  apreim  7367  apirr  7369  apsym  7370  apcotr  7371  apadd1  7372  apneg  7375  mulext1  7376  msqge0  7380  mulge0  7383  apti  7386  ltleap  7393  recexap  7396  mulap0b  7398  recgt0  7577  prodgt02  7580  prodge02  7582  lemul12b  7588  lemul12a  7589  nnrecgt0  7712  addltmul  7918  nominpos  7919  elnnz  8011  peano2z  8037  zaddcllempos  8038  zaddcl  8041  zletric  8045  zlelttric  8046  zltnle  8047  zleloe  8048  zrevaddcl  8051  zdceq  8072  zdcle  8073  zdclt  8074  nn0n0n1ge2b  8076  nn0lt2  8078  zextle  8087  peano5uzti  8102  uzind2  8106  fzind  8109  fnn0ind  8110  nn0ind-raph  8111  btwnz  8113  eluzuzle  8237  uz11  8251  eluzp1m1  8252  lbzbi  8307  qapne  8330  qreccl  8331  qrevaddcl  8333  irradd  8335  irrmul  8336  xrlelttr  8472  xrltletr  8473  ixxss1  8523  ixxss2  8524  ixxss12  8525  iccid  8544  elioc2  8555  elico2  8556  elicc2  8557  fznlem  8655  fzn  8656  fzen  8657  0fz1  8659  uzsubsubfz  8661  fzopth  8674  fzss1  8676  fzss2  8677  elfz1b  8702  uzsplit  8704  fzm1  8712  fznuz  8714  fzrevral  8717  elfz0ubfz0  8732  elfz0fzfz0  8733  fz0fzelfz0  8734  difelfzle  8742  1fv  8746  fzoss1  8777  fzosplit  8783  fzouzsplit  8785  fzonmapblen  8793  fzofzim  8794  eluzgtdifelfzo  8803  elfzodifsumelfzo  8807  elfzom1p1elfzo  8820  ssfzo12  8830  ssfzo12bi  8831  fzofzp1b  8834  elfzonelfzo  8836  frec2uzzd  8847  frec2uzuzd  8849  frec2uzltd  8850  frec2uzlt2d  8851  frec2uzrand  8852  frec2uzf1od  8853  frec2uzrdg  8856  frecuzrdgfn  8859  frecfzennn  8864  expival  8891  expcl2lemap  8901  leexp2r  8942  leexp1a  8943  zesq  9000  expnbnd  9005  reim0b  9070  cjap  9114  sqrt0  9193  sqrtsq  9194  absnid  9207  cbvrald  9242  bdsepnft  9321  peano5set  9374  findset  9379  bj-omtrans  9390  bj-findis  9409  strcollnft  9414
  Copyright terms: Public domain W3C validator