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.29_2a  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  3527  prel12  3532  dfnfc2  3588  intssunim  3627  intab  3634  iineq2d  3667  ssiun2  3690  mpteq2da  3836  trintssm  3860  copsexg  3971  copsex2t  3972  sess1  4058  sess2  4059  tron  4084  onelss  4089  onintss  4092  reusv1  4155  reusv3  4157  rabxfrd  4166  iunpw  4176  ssorduni  4178  ordsson  4183  ordsucg  4193  onsucelsucexmidlem  4213  elirr  4223  en2lp  4231  ordsuc  4240  ordpwsucss  4242  tfisi  4252  sosng  4355  2optocl  4359  relop  4428  xpid11m  4499  releldmb  4513  relelrnb  4514  elrnmptg  4528  elreimasng  4633  relbrcnvg  4646  trin2  4658  ssxpbm  4698  ssxp1  4699  ssxp2  4700  elxp4  4750  elxp5  4751  relresfld  4789  relcoi1  4791  iotaval  4820  iotass  4826  funmo  4858  imadif  4920  imain  4922  2elresin  4951  feu  5013  fcnvres  5014  f1oun  5087  f1oprg  5109  relfvssunirn  5132  funbrfv  5153  funbrfv2b  5159  dffn5im  5160  dfimafn  5163  funimass4  5165  ssimaex  5175  fvmptssdm  5196  fvmptf  5204  fvimacnv  5223  funimass3  5224  elpreima  5227  elrnrexdm  5247  eldmrexrn  5249  dffo4  5256  dffo5  5257  fmpt  5260  ffvresb  5269  fmptco  5271  fsn  5276  funfvima  5331  funfvima2  5332  f1mpt  5351  f1imass  5354  f1ocnvfvrneq  5363  foeqcnvco  5371  f1eqcocnv  5372  fliftfun  5377  fliftf  5380  isopolem  5402  isosolem  5404  eusvobj2  5438  acexmidlemab  5446  oprabid  5477  ovidi  5558  ovg  5578  suppssfv  5647  suppssov1  5648  funrnex  5680  f1dmex  5682  oprabexd  5693  fo2ndresm  5728  op1steq  5744  dfoprab3  5756  fo2ndf  5787  f1o2ndf1  5788  poxp  5791  isprmpt2  5796  reldmtpos  5806  rntpos  5810  tposf2  5821  tposf12  5822  issmo2  5842  smores  5845  smoiso  5855  tfrlem9  5873  tfrlemibacc  5878  tfrlemibfn  5880  tfrlemi14d  5885  tfrexlem  5886  rdgivallem  5905  frecsuclem3  5923  frecrdg  5925  oawordi  5981  nnmcom  6000  nnsucelsuc  6002  nntri3or  6004  nntri1  6006  nnaordi  6010  nnmord  6019  nnaordex  6029  nnm00  6031  ertr  6050  erex  6059  iserd  6061  iinerm  6107  erinxp  6109  qsel  6112  qliftfun  6117  qliftfund  6118  2ecoptocl  6123  brecop  6125  dom2lem  6181  fundmen  6215  unen  6222  enm  6223  xpdom2  6234  fopwdom  6239  mulcanpig  6312  nlt1pig  6318  addcmpblnq  6344  ltsonq  6375  ltexnqq  6384  prarloclemarch2  6395  enq0tr  6409  addcmpblnq0  6418  addnq0mo  6422  mulnq0mo  6423  prcdnql  6459  prcunqu  6460  prarloclemlo  6469  prarloclem3step  6471  prarloclem3  6472  genpdflem  6482  genpelvl  6487  genpelvu  6488  genpcdl  6495  genpcuu  6496  genprndl  6497  genprndu  6498  genpdisj  6499  addnqprllem  6503  addnqprulem  6504  addlocprlemeq  6509  addlocprlemgt  6510  nqprloc  6521  addnqpr1lemrl  6529  addnqpr1lemru  6530  addnqpr1lemil  6531  addnqpr1lemiu  6532  prmuloc  6537  prmuloc2  6538  mullocpr  6542  distrlem4prl  6550  distrlem4pru  6551  ltprordil  6555  1idprl  6556  1idpru  6557  ltpopr  6559  ltsopr  6560  ltaddpr  6561  ltexprlemm  6564  ltexprlemlol  6566  ltexprlemupu  6568  ltexprlemdisj  6570  ltexprlemloc  6571  ltexprlemrl  6574  ltexprlemru  6576  addcanprleml  6578  addcanprlemu  6579  addcanprg  6580  ltaprg  6582  recexprlemlol  6588  recexprlemdisj  6592  recexprlemloc  6593  recexprlem1ssl  6595  recexprlem1ssu  6596  aptiprleml  6601  aptiprlemu  6602  ltmprr  6604  archpr  6605  mulcmpblnrlemg  6620  addsrmo  6623  mulsrmo  6624  ltsrprg  6627  pitonn  6696  lelttr  6855  ltletr  6856  readdcan  6902  cnegexlem1  6935  cnegexlem2  6936  add20  7216  recexre  7314  inelr  7320  rimul  7321  apreap  7323  ltmul1  7328  cru  7338  apreim  7339  apirr  7341  apsym  7342  apcotr  7343  apadd1  7344  apneg  7347  mulext1  7348  msqge0  7352  mulge0  7355  apti  7358  ltleap  7365  recexap  7368  mulap0b  7370  recgt0  7548  prodgt02  7551  prodge02  7553  lemul12b  7559  lemul12a  7560  nnrecgt0  7683  addltmul  7888  nominpos  7889  elnnz  7981  peano2z  8007  zaddcllempos  8008  zaddcl  8011  zletric  8015  zlelttric  8016  zltnle  8017  zleloe  8018  zrevaddcl  8021  zdceq  8042  zdcle  8043  nn0n0n1ge2b  8045  nn0lt2  8047  zextle  8056  peano5uzti  8071  uzind2  8075  fzind  8078  fnn0ind  8079  nn0ind-raph  8080  btwnz  8082  eluzuzle  8206  uz11  8220  eluzp1m1  8221  lbzbi  8276  qapne  8299  qreccl  8300  qrevaddcl  8302  irradd  8304  irrmul  8305  xrlelttr  8440  xrltletr  8441  ixxss1  8491  ixxss2  8492  ixxss12  8493  iccid  8512  elioc2  8523  elico2  8524  elicc2  8525  fznlem  8621  fzn  8622  fzen  8623  0fz1  8625  uzsubsubfz  8627  fzopth  8640  fzss1  8642  fzss2  8643  elfz1b  8668  uzsplit  8670  fzm1  8678  fznuz  8680  fzrevral  8683  elfz0ubfz0  8698  elfz0fzfz0  8699  fz0fzelfz0  8700  difelfzle  8708  1fv  8712  fzoss1  8743  fzosplit  8749  fzouzsplit  8751  fzonmapblen  8759  fzofzim  8760  eluzgtdifelfzo  8769  elfzodifsumelfzo  8773  elfzom1p1elfzo  8786  ssfzo12  8796  ssfzo12bi  8797  fzofzp1b  8800  elfzonelfzo  8802  frec2uzzd  8813  frec2uzuzd  8815  frec2uzltd  8816  frec2uzlt2d  8817  frec2uzrand  8818  frec2uzf1od  8819  frecfzennn  8822  cbvrald  8861  bdsepnft  8940  peano5set  8993  findset  8998  bj-omtrans  9009  bj-findis  9028  strcollnft  9033
  Copyright terms: Public domain W3C validator