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

Theorem ex 113
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 106 . 2 (𝜑 → (𝜓 → (𝜑𝜓)))
2 exp.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl6 33 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  expcom  114  bi3  117  expd  254  impancom  256  expimpd  355  exp31  356  exp32  357  exp4b  359  exp41  362  exp43  364  exp53  369  impr  371  simplbi2  377  anidms  389  syl2anc  403  pm5.74da  432  imdistanda  437  pm5.32da  440  impbida  561  anim12dan  565  pm2.01da  598  pm2.65da  620  mtand  624  pm5.21im  645  jao  705  jaoian  742  jaodan  744  impidc  791  pm2.5dc  799  con1bidc  804  con2bidc  805  con1bdc  808  pm5.18dc  813  dfandc  814  pm4.63dc  816  dcim  820  pm4.54dc  841  pm5.21nd  861  dcan  878  dcor  879  annimdc  881  pm4.55dc  882  pm3.11dc  901  pm3.12dc  902  prlem1  917  pm3.2an3  1120  3jcad  1122  3impia  1138  3an1rs  1153  3exp1  1157  3exp2  1159  exp520  1162  syl3anl2  1221  3jaoian  1239  3jaodan  1240  mp3anl1  1265  mp3anl2  1266  mp3anl3  1267  inegd  1306  xor3dc  1321  pm5.15dc  1323  xor2dc  1324  xornbidc  1325  xordc  1326  nbbndc  1328  biassdc  1329  dfbi3dc  1331  pm5.24dc  1332  alanimi  1391  equsexd  1661  sbequ1  1695  sbiedv  1716  ax11v2  1745  equs5or  1755  sbequi  1764  exlimdd  1797  exlimddv  1823  cbvaldva  1848  cbvexdva  1849  nfsbxyt  1864  sbcomxyyz  1891  nfsb4t  1935  eupickbi  2027  moexexdc  2029  euexex  2030  2euswapdc  2036  dvelimdc  2244  nebidc  2331  rgen2a  2425  ralimiaa  2433  ralimdaa  2436  ralrimiva  2442  ralrimdva  2449  ralrimivva  2451  ralrimdvv  2453  ralrimdvva  2454  reximdva  2471  reximddv2  2473  rexlimiva  2480  rexlimdva  2485  rexlimdvva  2492  r19.29vva  2509  2gencl  2646  vtocldf  2664  spcimdv  2696  spcimedv  2698  rspct  2708  eqvinc  2731  eqvincg  2732  ceqex  2735  reu6  2795  eqreu  2798  sbciedf  2863  rmob  2920  csbiebt  2956  csbiedf  2957  reupick  3272  reximdva0m  3287  ssn0  3313  rgenm  3371  eqifdc  3411  preqr1g  3593  prel12  3598  dfnfc2  3654  intssunim  3693  intab  3700  iineq2d  3733  ssiun2  3756  mpteq2da  3902  trintssmOLD  3928  exmid01  4006  exmidundif  4009  copsexg  4045  copsex2t  4046  sess1  4138  sess2  4139  frirrg  4151  tron  4183  onelss  4188  onintss  4191  reusv1  4254  reusv3  4256  rabxfrd  4265  iunpw  4275  ssorduni  4277  ordsson  4282  ordsucg  4292  onintrab2im  4308  onsucelsucexmidlem  4318  elirr  4330  en2lp  4343  ordsuc  4352  ordpwsucss  4356  ordtri2or2exmid  4360  reg3exmidlemwe  4367  tfisi  4375  omsinds  4408  sosng  4479  2optocl  4483  relop  4554  xpid11m  4626  releldmb  4640  relelrnb  4641  elrnmptg  4655  elreimasng  4765  relbrcnvg  4778  trin2  4790  ssxpbm  4832  ssxp1  4833  ssxp2  4834  elxp4  4884  elxp5  4885  relresfld  4926  relcoi1  4928  iotaval  4957  iotass  4963  funmo  4996  imadif  5059  imain  5061  2elresin  5090  feu  5156  fcnvres  5157  f0rn0  5168  f1oun  5236  f1oprg  5258  relfvssunirn  5284  funbrfv  5306  funbrfv2b  5312  dffn5im  5313  dfimafn  5316  funimass4  5318  ssimaex  5328  fvmptssdm  5350  fvmptf  5358  fvimacnv  5377  funimass3  5378  elpreima  5381  elrnrexdm  5401  eldmrexrn  5403  dffo4  5410  dffo5  5411  fmpt  5412  fmptdf  5418  ffvresb  5424  resflem  5425  fmptco  5427  fsn  5432  funfvima  5487  funfvima2  5488  f1mpt  5511  f1imass  5514  f1ocnvfvrneq  5522  foeqcnvco  5530  f1eqcocnv  5531  fliftfun  5536  fliftf  5539  isopolem  5562  isosolem  5564  eusvobj2  5599  acexmidlemab  5607  oprabid  5638  ovidi  5720  ovg  5740  suppssfv  5809  suppssov1  5810  funrnex  5842  f1dmex  5844  oprabexd  5855  fo2ndresm  5890  op1steq  5906  dfoprab3  5918  fo2ndf  5949  f1o2ndf1  5950  poxp  5954  spc2ed  5955  f1od2  5957  isprmpt2  5962  reldmtpos  5972  rntpos  5976  tposf2  5987  tposf12  5988  issmo2  6008  smores  6011  smoiso  6021  tfrlem9  6038  tfrlemibacc  6045  tfrlemibfn  6047  tfrlemi14d  6052  tfrexlem  6053  tfr1onlembacc  6061  tfr1onlembfn  6063  tfr1onlemres  6068  tfri1dALT  6070  tfrcllembacc  6074  tfrcllembfn  6076  tfrcllemres  6081  tfrcl  6083  rdgivallem  6100  frecabcl  6118  frecrdg  6127  oawordi  6184  nnmcom  6204  nnsucelsuc  6206  nntri3or  6208  nnsucuniel  6210  nntri1  6211  nnsseleq  6216  dcdifsnid  6217  nnaordi  6219  nnmord  6228  nnaordex  6238  nnm00  6240  ertr  6259  erex  6268  iserd  6270  iinerm  6316  erinxp  6318  qsel  6321  qliftfun  6326  qliftfund  6327  2ecoptocl  6332  brecop  6334  mapss  6400  dom2lem  6441  fundmen  6475  unen  6485  enm  6488  xpdom2  6499  fopwdom  6504  xpf1o  6512  mapen  6514  mapxpen  6516  ssenen  6519  phplem4  6523  nneneq  6525  snnen2og  6527  phplem4dom  6530  nndomo  6532  phpm  6533  phplem4on  6535  fidifsnen  6538  dif1enen  6548  fin0  6553  fin0or  6554  findcard2  6557  findcard2s  6558  findcard2d  6559  findcard2sd  6560  ac6sfi  6566  fimax2gtri  6569  finexdc  6570  en2eqpr  6575  onunsnss  6579  unfidisj  6584  undifdcss  6585  undifdc  6586  xpfi  6590  fisseneq  6592  ssfirab  6593  fnfi  6596  f1finf1o  6605  en1eqsnbi  6607  isbth  6620  eqsupti  6635  suplub2ti  6640  isotilem  6645  supisoex  6648  eqinfti  6659  inflbti  6663  ordiso2  6672  djulclb  6691  updjudhf  6714  updjud  6717  enomnilem  6738  finomni  6740  exmidomniim  6741  exmidomni  6742  fodjuomnilemdc  6743  fodjuomnilemres  6747  nnnninf  6750  pm54.43  6762  pr2nelem  6763  pr2ne  6764  exmidfodomrlemim  6771  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  mulcanpig  6838  nlt1pig  6844  addcmpblnq  6870  ltsonq  6901  ltexnqq  6911  prarloclemarch2  6922  enq0tr  6937  addcmpblnq0  6946  addnq0mo  6950  mulnq0mo  6951  prcdnql  6987  prcunqu  6988  prarloclemlo  6997  prarloclem3step  6999  prarloclem3  7000  genpdflem  7010  genpelvl  7015  genpelvu  7016  genpcdl  7022  genpcuu  7023  genprndl  7024  genprndu  7025  genpdisj  7026  addnqprllem  7030  addnqprulem  7031  addlocprlemeq  7036  addlocprlemgt  7037  nqprloc  7048  nqprl  7054  nqpru  7055  addnqprlemrl  7060  addnqprlemru  7061  addnqprlemfl  7062  addnqprlemfu  7063  prmuloc  7069  prmuloc2  7070  mullocpr  7074  mulnqprlemrl  7076  mulnqprlemru  7077  mulnqprlemfl  7078  mulnqprlemfu  7079  distrlem4prl  7087  distrlem4pru  7088  ltprordil  7092  1idprl  7093  1idpru  7094  ltpopr  7098  ltsopr  7099  ltaddpr  7100  ltexprlemm  7103  ltexprlemlol  7105  ltexprlemupu  7107  ltexprlemdisj  7109  ltexprlemloc  7110  ltexprlemrl  7113  ltexprlemru  7115  addcanprleml  7117  addcanprlemu  7118  addcanprg  7119  ltaprg  7122  recexprlemlol  7129  recexprlemdisj  7133  recexprlemloc  7134  recexprlem1ssl  7136  recexprlem1ssu  7137  aptiprleml  7142  aptiprlemu  7143  ltmprr  7145  archpr  7146  cauappcvgprlemm  7148  cauappcvgprlemopl  7149  cauappcvgprlemlol  7150  cauappcvgprlemopu  7151  cauappcvgprlemrnd  7153  cauappcvgprlemloc  7155  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  caucvgprlemnkj  7169  caucvgprlemm  7171  caucvgprlemopl  7172  caucvgprlemlol  7173  caucvgprlemopu  7174  caucvgprlemrnd  7176  caucvgprlemloc  7178  caucvgprlemladdfu  7180  caucvgprlemladdrl  7181  caucvgprlemlim  7184  caucvgprprlemnkltj  7192  caucvgprprlemnkeqj  7193  caucvgprprlemnjltk  7194  caucvgprprlemml  7197  caucvgprprlemopl  7200  caucvgprprlemlol  7201  caucvgprprlemopu  7202  caucvgprprlemrnd  7204  caucvgprprlemloc  7206  caucvgprprlemexbt  7209  caucvgprprlemexb  7210  caucvgprprlemlim  7214  mulcmpblnrlemg  7230  addsrmo  7233  mulsrmo  7234  ltsrprg  7237  srpospr  7272  caucvgsrlemgt1  7284  pitonn  7329  nntopi  7373  axcaucvglemcau  7377  axcaucvglemres  7378  lelttr  7517  ltletr  7518  readdcan  7566  cnegexlem1  7601  cnegexlem2  7602  addid0  7795  lelttrdi  7848  add20  7896  recexre  7996  inelr  8002  rimul  8003  apreap  8005  ltmul1  8010  cru  8020  apreim  8021  apirr  8023  apsym  8024  apcotr  8025  apadd1  8026  apneg  8029  mulext1  8030  msqge0  8034  mulge0  8037  apti  8040  ltleap  8048  recexap  8061  mulap0b  8063  recgt0  8246  prodgt02  8249  prodge02  8251  lemul12b  8257  lemul12a  8258  nnrecgt0  8394  addltmul  8585  nominpos  8586  elnnz  8693  peano2z  8719  zaddcllempos  8720  zaddcl  8723  zletric  8727  zlelttric  8728  zltnle  8729  zleloe  8730  zrevaddcl  8733  nzadd  8735  zdceq  8755  zdcle  8756  zdclt  8757  nn0n0n1ge2b  8759  nn0lt2  8761  zextle  8770  peano5uzti  8787  uzind2  8791  fzind  8794  fnn0ind  8795  nn0ind-raph  8796  btwnz  8798  eluzuzle  8959  uz11  8973  eluzp1m1  8974  supinfneg  9015  infsupneg  9016  lbzbi  9033  qapne  9056  qreccl  9059  qrevaddcl  9061  irradd  9063  irrmul  9064  ledivge1le  9135  nn0ledivnn  9170  xrlelttr  9203  xrltletr  9204  ixxss1  9254  ixxss2  9255  ixxss12  9256  iccid  9275  elioc2  9286  elico2  9287  elicc2  9288  fznlem  9387  fzn  9388  fzen  9389  0fz1  9391  uzsubsubfz  9393  fzopth  9406  fzss1  9408  fzss2  9409  elfz1b  9434  uzsplit  9436  fzm1  9444  fznuz  9446  fzrevral  9449  elfz0ubfz0  9464  elfz0fzfz0  9465  fz0fzelfz0  9466  difelfzle  9473  1fv  9478  fzoss1  9510  fzosplit  9516  fzouzsplit  9518  fzonmapblen  9526  fzofzim  9527  eluzgtdifelfzo  9536  elfzodifsumelfzo  9540  elfzom1p1elfzo  9553  ssfzo12  9563  ssfzo12bi  9564  fzofzp1b  9567  elfzonelfzo  9569  subfzo0  9581  qtri3or  9582  qletric  9583  qlelttric  9584  qltnle  9585  qdceq  9586  exbtwnzlemstep  9587  exbtwnzlemshrink  9588  exbtwnzlemex  9589  exbtwnz  9590  rebtwn2zlemstep  9592  rebtwn2z  9594  ioom  9600  ico0  9601  ioc0  9602  flltdivnn0lt  9639  flqeqceilz  9653  modqid2  9686  modqmuladd  9701  modqmuladdim  9702  modqmuladdnn0  9703  modqm1p1mod0  9710  modaddmodlo  9723  modfzo0difsn  9730  addmodlteq  9733  frec2uzuzd  9737  frec2uzltd  9738  frec2uzlt2d  9739  frec2uzrand  9740  frec2uzf1od  9741  frec2uzrdg  9744  frecuzrdgtcl  9747  frecuzrdgdomlem  9752  frecuzrdgfunlem  9754  frecfzennn  9761  uzsinds  9776  iseqclt  9798  iseqoveq  9799  iseqf1olemqf1o  9827  iseqf1olemp  9836  iseqid3s  9842  iseqid  9843  iseqz  9846  expival  9856  expcl2lemap  9866  leexp2r  9908  leexp1a  9909  zesq  9969  expnbnd  9974  nn0opthlem2d  10026  nn0opthd  10027  facdiv  10043  facndiv  10044  facwordi  10045  faclbnd  10046  faclbnd6  10049  facubnd  10050  bcval4  10057  bcpasc  10071  bccl  10072  fiinfnf1o  10091  fihashf1rn  10094  hashunlem  10109  fiprsshashgt1  10122  hashfzo  10127  hashfzp1  10129  hashxp  10131  hashfacen  10138  zfz1iso  10143  iseqcoll  10144  ovshftex  10150  reim0b  10192  cjap  10236  caucvgrelemcau  10309  caucvgre  10310  cvg1nlemres  10314  r19.29uz  10321  r19.2uz  10322  recvguniq  10324  sqrt0  10333  resqrexlemover  10339  resqrexlemdecn  10341  resqrexlemlo  10342  resqrexlemcalc3  10345  resqrexlemglsq  10351  resqrexlemga  10352  rsqrmo  10356  sqrtsq  10373  abs00ap  10391  absnid  10402  qabsor  10404  absexpzap  10409  abs3lem  10440  cau3lem  10443  caubnd2  10446  icodiamlt  10509  maxleim  10534  maxabslemlub  10536  maxabslemval  10537  fimaxre2  10553  negfi  10554  minmax  10556  clim  10564  climuni  10576  climcn1  10591  climcn2  10592  mulcn2  10595  iiserex  10621  climcau  10628  climcaucn  10632  isumrblem  10657  fisumcvg  10658  isummolem2a  10662  zisum  10665  fisum  10667  isumz  10669  fsumf1o  10670  fisumss  10672  fisumcvg3  10676  dvdsval2  10681  moddvds  10687  dvds0  10693  absdvdsb  10696  dvdsabsb  10697  dvdsmul1  10700  dvdscmul  10705  dvdsmulc  10706  dvds2ln  10711  dvds2add  10712  dvds2sub  10713  dvdslelemd  10726  dvdsleabs2  10729  dvds1  10736  dvdsext  10738  fzo0dvdseq  10740  dvdsfac  10743  mulmoddvds  10746  odd2np1  10755  oddge22np1  10763  evennn02n  10764  evennn2n  10765  mulsucdiv2z  10767  sqoddm1div8z  10768  ltoddhalfle  10775  halfleoddlt  10776  m1expo  10782  nn0ehalf  10785  nn0o  10789  nn0oddm1d2  10791  nnoddm1d2  10792  divalglemeunn  10803  divalglemex  10804  divalglemeuneg  10805  flodddiv4  10816  zsupcllemstep  10823  dvdsbnd  10830  dvdslegcd  10838  gcdeq0  10850  gcd0id  10852  gcdneg  10855  gcdaddm  10857  gcdabs  10861  bezoutlemnewy  10867  bezoutlemstep  10868  bezoutlemzz  10873  bezoutlemaz  10874  bezoutlembz  10875  bezoutlembi  10876  bezoutlemeu  10878  bezoutlemle  10879  bezoutlemsup  10880  dvdsgcd  10883  dfgcd2  10885  rppwr  10899  dvdssqlem  10901  bezoutr1  10904  ialgfx  10916  eucalglt  10921  eucialgcvga  10922  lcmledvds  10934  lcmeq0  10935  lcmneg  10938  lcmabs  10940  lcmgcdlem  10941  lcmdvds  10943  lcmgcdeq  10947  coprmgcdb  10952  ncoprmgcdne1b  10953  coprmdvds  10956  qredeq  10960  qredeu  10961  rpdvds  10963  divgcdcoprm0  10965  divgcdcoprmex  10966  cncongr1  10967  cncongr2  10968  isprm2lem  10980  prmind2  10984  dvdsnprmd  10989  divgcdodd  11004  coprm  11005  isprm6  11008  prmfac1  11013  rpexp  11014  sqrt2irr  11023  pw2dvdseu  11028  sqrt2irrap  11040  nonsq  11067  hashdvds  11079  phimullem  11083  cbvrald  11133  uzdcinzz  11143  bdsepnft  11223  peano5set  11280  findset  11285  bj-omtrans  11296  bj-findis  11319  strcollnft  11324  nnpredcl  11335  peano4nninf  11341  nninfalllem1  11344  nninfall  11345  nninfsellemqall  11352  nninfomnilem  11355  exmidsbthrlem  11357  exmidsbth  11359
  Copyright terms: Public domain W3C validator