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  6502  genpcuu  6503  genprndl  6504  genprndu  6505  genpdisj  6506  addnqprllem  6510  addnqprulem  6511  addlocprlemeq  6516  addlocprlemgt  6517  nqprloc  6528  addnqpr1lemrl  6537  addnqpr1lemru  6538  addnqpr1lemil  6539  addnqpr1lemiu  6540  prmuloc  6545  prmuloc2  6546  mullocpr  6550  distrlem4prl  6558  distrlem4pru  6559  ltprordil  6563  1idprl  6564  1idpru  6565  ltpopr  6567  ltsopr  6568  ltaddpr  6569  ltexprlemm  6572  ltexprlemlol  6574  ltexprlemupu  6576  ltexprlemdisj  6578  ltexprlemloc  6579  ltexprlemrl  6582  ltexprlemru  6584  addcanprleml  6586  addcanprlemu  6587  addcanprg  6588  ltaprg  6590  recexprlemlol  6596  recexprlemdisj  6600  recexprlemloc  6601  recexprlem1ssl  6603  recexprlem1ssu  6604  aptiprleml  6609  aptiprlemu  6610  ltmprr  6612  archpr  6613  mulcmpblnrlemg  6628  addsrmo  6631  mulsrmo  6632  ltsrprg  6635  pitonn  6704  lelttr  6863  ltletr  6864  readdcan  6910  cnegexlem1  6943  cnegexlem2  6944  add20  7224  recexre  7322  inelr  7328  rimul  7329  apreap  7331  ltmul1  7336  cru  7346  apreim  7347  apirr  7349  apsym  7350  apcotr  7351  apadd1  7352  apneg  7355  mulext1  7356  msqge0  7360  mulge0  7363  apti  7366  ltleap  7373  recexap  7376  mulap0b  7378  recgt0  7557  prodgt02  7560  prodge02  7562  lemul12b  7568  lemul12a  7569  nnrecgt0  7692  addltmul  7898  nominpos  7899  elnnz  7991  peano2z  8017  zaddcllempos  8018  zaddcl  8021  zletric  8025  zlelttric  8026  zltnle  8027  zleloe  8028  zrevaddcl  8031  zdceq  8052  zdcle  8053  zdclt  8054  nn0n0n1ge2b  8056  nn0lt2  8058  zextle  8067  peano5uzti  8082  uzind2  8086  fzind  8089  fnn0ind  8090  nn0ind-raph  8091  btwnz  8093  eluzuzle  8217  uz11  8231  eluzp1m1  8232  lbzbi  8287  qapne  8310  qreccl  8311  qrevaddcl  8313  irradd  8315  irrmul  8316  xrlelttr  8452  xrltletr  8453  ixxss1  8503  ixxss2  8504  ixxss12  8505  iccid  8524  elioc2  8535  elico2  8536  elicc2  8537  fznlem  8635  fzn  8636  fzen  8637  0fz1  8639  uzsubsubfz  8641  fzopth  8654  fzss1  8656  fzss2  8657  elfz1b  8682  uzsplit  8684  fzm1  8692  fznuz  8694  fzrevral  8697  elfz0ubfz0  8712  elfz0fzfz0  8713  fz0fzelfz0  8714  difelfzle  8722  1fv  8726  fzoss1  8757  fzosplit  8763  fzouzsplit  8765  fzonmapblen  8773  fzofzim  8774  eluzgtdifelfzo  8783  elfzodifsumelfzo  8787  elfzom1p1elfzo  8800  ssfzo12  8810  ssfzo12bi  8811  fzofzp1b  8814  elfzonelfzo  8816  frec2uzzd  8827  frec2uzuzd  8829  frec2uzltd  8830  frec2uzlt2d  8831  frec2uzrand  8832  frec2uzf1od  8833  frec2uzrdg  8836  frecuzrdgfn  8839  frecfzennn  8844  expival  8871  expcl2lemap  8881  leexp2r  8922  leexp1a  8923  zesq  8980  expnbnd  8985  reim0b  9050  cjap  9094  cbvrald  9196  bdsepnft  9275  peano5set  9328  findset  9333  bj-omtrans  9344  bj-findis  9363  strcollnft  9368
  Copyright terms: Public domain W3C validator