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

Theorem ex 114
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 107 . 2 (𝜑 → (𝜓 → (𝜑𝜓)))
2 exp.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl6 33 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  expcom  115  bi3  118  expd  256  impancom  258  expimpd  358  exp31  359  exp32  360  exp4b  362  exp41  365  exp43  367  exp53  372  impr  374  simplbi2  380  anidms  392  syl2anc  406  pm5.74da  437  imdistanda  442  pm5.32da  445  a2and  530  impbida  568  anim12dan  572  pm2.01da  608  pm2.65da  633  mtand  637  pm5.21im  668  jao  727  jaoian  767  jaodan  769  dcim  809  stdcn  815  impidc  826  pm2.5gdc  834  con1bidc  842  con2bidc  843  con1bdc  846  pm5.18dc  851  dfandc  852  pm4.63dc  854  pm4.54dc  870  pm5.21nd  884  dcan  901  dcor  902  annimdc  904  pm4.55dc  905  pm3.11dc  924  pm3.12dc  925  prlem1  940  pm3.2an3  1143  3jcad  1145  3impia  1161  3an1rs  1180  3exp1  1184  3exp2  1186  exp520  1189  syl3anl2  1248  3jaoian  1266  3jaodan  1267  mp3anl1  1292  mp3anl2  1293  mp3anl3  1294  inegd  1333  xor3dc  1348  pm5.15dc  1350  xor2dc  1351  xornbidc  1352  xordc  1353  nbbndc  1355  biassdc  1356  dfbi3dc  1358  pm5.24dc  1359  alanimi  1418  equsexd  1690  sbequ1  1724  sbiedv  1745  ax11v2  1774  equs5or  1784  sbequi  1793  exlimdd  1826  exlimddv  1852  cbvaldva  1878  cbvexdva  1879  nfsbxyt  1894  sbcomxyyz  1921  nfsb4t  1965  eupickbi  2057  moexexdc  2059  euexex  2060  2euswapdc  2066  dvelimdc  2276  nebidc  2363  rgen2a  2461  ralimiaa  2469  ralimdaa  2473  ralrimiva  2480  ralrimdva  2487  ralrimivva  2489  ralrimdvv  2491  ralrimdvva  2492  reximdva  2509  reximssdv  2511  reximddv2  2512  rexlimiva  2519  rexlimdva  2524  rexlimdvva  2532  r19.29vva  2552  2gencl  2691  vtocldf  2709  spcimdv  2742  spcimedv  2744  rspct  2754  eqvinc  2780  eqvincg  2781  ceqex  2784  reu6  2844  eqreu  2847  sbciedf  2914  rmob  2971  csbiebt  3007  csbiedf  3008  eqelssd  3084  reupick  3328  reximdva0m  3346  ssn0  3373  rgenm  3433  eqifdc  3474  preqr1g  3661  prel12  3666  dfnfc2  3722  intssunim  3761  intab  3768  iineq2d  3801  ssiun2  3824  mpteq2da  3985  exmid01  4089  pwntru  4090  exmid1dc  4091  exmidn0m  4092  exmidsssnc  4094  exmidundif  4097  exmidundifim  4098  copsexg  4134  copsex2t  4135  sess1  4227  sess2  4228  frirrg  4240  tron  4272  onelss  4277  onintss  4280  abnexg  4335  reusv1  4347  reusv3  4349  rabxfrd  4358  iunpw  4369  ssorduni  4371  ordsson  4376  ordsucg  4386  onintrab2im  4402  onsucelsucexmidlem  4412  elirr  4424  en2lp  4437  ordsuc  4446  ordpwsucss  4450  ordtri2or2exmid  4454  reg3exmidlemwe  4461  tfisi  4469  omsinds  4503  nnpredcl  4504  sosng  4580  2optocl  4584  relop  4657  releldmb  4744  relelrnb  4745  elrnmptg  4759  elreimasng  4873  relbrcnvg  4886  trin2  4898  ssxpbm  4942  ssxp1  4943  ssxp2  4944  elxp4  4994  elxp5  4995  relresfld  5036  relcoi1  5038  iotaval  5067  iotass  5073  funmo  5106  imadif  5171  imain  5173  2elresin  5202  feu  5273  fcnvres  5274  f0rn0  5285  f1oun  5353  f1oprg  5377  relfvssunirn  5403  funbrfv  5426  funbrfv2b  5432  dffn5im  5433  dfimafn  5436  funimass4  5438  ssimaex  5448  fvmptssdm  5471  fvmptf  5479  elfvmptrab1  5481  fvimacnv  5501  funimass3  5502  elpreima  5505  elrnrexdm  5525  eldmrexrn  5527  dffo4  5534  dffo5  5535  fmpt  5536  fmptdf  5543  ffvresb  5549  resflem  5550  fmptco  5552  fsn  5558  funfvima  5615  funfvima2  5616  f1mpt  5638  f1imass  5641  f1ocnvfvrneq  5649  foeqcnvco  5657  f1eqcocnv  5658  fliftfun  5663  fliftf  5666  isopolem  5689  isosolem  5691  eusvobj2  5726  acexmidlemab  5734  oprabid  5769  ovidi  5855  ovg  5875  suppssfv  5944  suppssov1  5945  funrnex  5978  f1dmex  5980  oprabexd  5991  fo2ndresm  6026  oprssdmm  6035  op1steq  6043  dfoprab3  6055  fo2ndf  6090  f1o2ndf1  6091  poxp  6095  spc2ed  6096  f1od2  6098  rbropapd  6105  reldmtpos  6116  rntpos  6120  tposf2  6131  tposf12  6132  issmo2  6152  smores  6155  smoiso  6165  tfrlem9  6182  tfrlemibacc  6189  tfrlemibfn  6191  tfrlemi14d  6196  tfrexlem  6197  tfr1onlembacc  6205  tfr1onlembfn  6207  tfr1onlemres  6212  tfri1dALT  6214  tfrcllembacc  6218  tfrcllembfn  6220  tfrcllemres  6225  tfrcl  6227  rdgivallem  6244  frecabcl  6262  frecrdg  6271  oawordi  6331  nnmcom  6351  nnsucelsuc  6353  nntri3or  6355  nnsucuniel  6357  nntri1  6358  nnsseleq  6363  nntr2  6365  dcdifsnid  6366  nnaordi  6370  nnmord  6379  nnaordex  6389  nnm00  6391  ertr  6410  erex  6419  iserd  6421  iinerm  6467  erinxp  6469  qsel  6472  qliftfun  6477  qliftfund  6478  2ecoptocl  6483  brecop  6485  mapss  6551  ixpssmap2g  6587  ixpssmapg  6588  dom2lem  6632  fundmen  6666  unen  6676  enm  6680  xpdom2  6691  fopwdom  6696  xpf1o  6704  mapen  6706  mapxpen  6708  ssenen  6711  phplem4  6715  nneneq  6717  snnen2og  6719  phplem4dom  6722  nndomo  6724  phpm  6725  phplem4on  6727  fidifsnen  6730  dif1enen  6740  fin0  6745  fin0or  6746  findcard2  6749  findcard2s  6750  findcard2d  6751  findcard2sd  6752  ac6sfi  6758  fimax2gtri  6761  finexdc  6762  en2eqpr  6767  onunsnss  6771  unfidisj  6776  undifdcss  6777  undifdc  6778  fiintim  6783  xpfi  6784  fisseneq  6786  ssfirab  6788  fnfi  6791  iunfidisj  6800  f1finf1o  6801  en1eqsnbi  6803  fidcenum  6810  isbth  6821  ssfii  6828  fieq0  6830  eqsupti  6849  suplub2ti  6854  isotilem  6859  supisoex  6862  eqinfti  6873  inflbti  6877  ordiso2  6886  djulclb  6906  updjudhf  6930  updjud  6933  difinfsn  6951  difinfinf  6952  ctmlemr  6959  ctm  6960  ctssdclemn0  6961  ctssdccl  6962  ctssdc  6964  enumct  6966  enomnilem  6976  finomni  6978  exmidomniim  6979  exmidomni  6980  fodjuomnilemdc  6982  fodjuomnilemres  6986  nnnninf  6989  ismkvnex  6995  mkvprop  6998  fodjumkvlemres  6999  pm54.43  7012  pr2nelem  7013  pr2ne  7014  exmidfodomrlemim  7021  exmidfodomrlemr  7022  exmidfodomrlemrALT  7023  acfun  7027  ccfunen  7043  mulcanpig  7107  nlt1pig  7113  addcmpblnq  7139  ltsonq  7170  ltexnqq  7180  prarloclemarch2  7191  enq0tr  7206  addcmpblnq0  7215  addnq0mo  7219  mulnq0mo  7220  prcdnql  7256  prcunqu  7257  prarloclemlo  7266  prarloclem3step  7268  prarloclem3  7269  genpdflem  7279  genpelvl  7284  genpelvu  7285  genpcdl  7291  genpcuu  7292  genprndl  7293  genprndu  7294  genpdisj  7295  addnqprllem  7299  addnqprulem  7300  addlocprlemeq  7305  addlocprlemgt  7306  nqprloc  7317  nqprl  7323  nqpru  7324  addnqprlemrl  7329  addnqprlemru  7330  addnqprlemfl  7331  addnqprlemfu  7332  prmuloc  7338  prmuloc2  7339  mullocpr  7343  mulnqprlemrl  7345  mulnqprlemru  7346  mulnqprlemfl  7347  mulnqprlemfu  7348  distrlem4prl  7356  distrlem4pru  7357  ltprordil  7361  1idprl  7362  1idpru  7363  ltpopr  7367  ltsopr  7368  ltaddpr  7369  ltexprlemm  7372  ltexprlemlol  7374  ltexprlemupu  7376  ltexprlemdisj  7378  ltexprlemloc  7379  ltexprlemrl  7382  ltexprlemru  7384  addcanprleml  7386  addcanprlemu  7387  addcanprg  7388  ltaprg  7391  recexprlemlol  7398  recexprlemdisj  7402  recexprlemloc  7403  recexprlem1ssl  7405  recexprlem1ssu  7406  aptiprleml  7411  aptiprlemu  7412  ltmprr  7414  archpr  7415  cauappcvgprlemm  7417  cauappcvgprlemopl  7418  cauappcvgprlemlol  7419  cauappcvgprlemopu  7420  cauappcvgprlemrnd  7422  cauappcvgprlemloc  7424  cauappcvgprlemladdfu  7426  cauappcvgprlemladdfl  7427  cauappcvgprlemladdru  7428  cauappcvgprlemladdrl  7429  caucvgprlemnkj  7438  caucvgprlemm  7440  caucvgprlemopl  7441  caucvgprlemlol  7442  caucvgprlemopu  7443  caucvgprlemrnd  7445  caucvgprlemloc  7447  caucvgprlemladdfu  7449  caucvgprlemladdrl  7450  caucvgprlemlim  7453  caucvgprprlemnkltj  7461  caucvgprprlemnkeqj  7462  caucvgprprlemnjltk  7463  caucvgprprlemml  7466  caucvgprprlemopl  7469  caucvgprprlemlol  7470  caucvgprprlemopu  7471  caucvgprprlemrnd  7473  caucvgprprlemloc  7475  caucvgprprlemexbt  7478  caucvgprprlemexb  7479  caucvgprprlemlim  7483  suplocexprlemrl  7489  suplocexprlemmu  7490  suplocexprlemru  7491  suplocexprlemloc  7493  suplocexprlemex  7494  suplocexprlemlub  7496  mulcmpblnrlemg  7512  addsrmo  7515  mulsrmo  7516  ltsrprg  7519  srpospr  7555  caucvgsrlemgt1  7567  map2psrprg  7577  suplocsrlemb  7578  suplocsrlempr  7579  suplocsrlem  7580  cnm  7604  pitonn  7620  nntopi  7666  axcaucvglemcau  7670  axcaucvglemres  7671  axpre-suploclemres  7673  lelttr  7816  ltletr  7817  readdcan  7866  cnegexlem1  7901  cnegexlem2  7902  addid0  8099  lelttrdi  8152  add20  8200  eqord1  8209  recexre  8303  inelr  8309  rimul  8310  apreap  8312  ltmul1  8317  cru  8327  apreim  8328  apirr  8330  apsym  8331  apcotr  8332  apadd1  8333  apneg  8336  mulext1  8337  msqge0  8341  mulge0  8344  apti  8347  ltleap  8357  aprcl  8371  recexap  8377  mulap0b  8379  mul0eqap  8394  recgt0  8568  prodgt02  8571  prodge02  8573  lemul12b  8579  lemul12a  8580  nnrecgt0  8718  addltmul  8910  nominpos  8911  elnnz  9018  peano2z  9044  zaddcllempos  9045  zaddcl  9048  zletric  9052  zlelttric  9053  zltnle  9054  zleloe  9055  zrevaddcl  9058  nzadd  9060  zdceq  9080  zdcle  9081  zdclt  9082  nn0n0n1ge2b  9084  nn0lt2  9086  zextle  9096  peano5uzti  9113  uzind2  9117  fzind  9120  fnn0ind  9121  nn0ind-raph  9122  btwnz  9124  eluzuzle  9286  uz11  9300  eluzp1m1  9301  supinfneg  9342  infsupneg  9343  lbzbi  9360  qapne  9383  qreccl  9386  qrevaddcl  9388  irradd  9390  irrmul  9391  ledivge1le  9464  nn0ledivnn  9505  xrlelttr  9540  xrltletr  9541  npnflt  9549  nmnfgt  9552  xnn0lenn0nn0  9599  xnn0xadd0  9601  xleadd1  9609  xle2add  9613  xposdif  9616  xlesubadd  9617  ixxss1  9638  ixxss2  9639  ixxss12  9640  iccid  9659  elioc2  9670  elico2  9671  elicc2  9672  fznlem  9772  fzn  9773  fzen  9774  0fz1  9776  uzsubsubfz  9778  fzopth  9792  fzss1  9794  fzss2  9795  elfz1b  9821  uzsplit  9823  fzm1  9831  fznuz  9833  fzrevral  9836  elfz0ubfz0  9853  elfz0fzfz0  9854  fz0fzelfz0  9855  difelfzle  9862  1fv  9867  fzoss1  9899  fzosplit  9905  fzouzsplit  9907  fzonmapblen  9915  fzofzim  9916  eluzgtdifelfzo  9925  elfzodifsumelfzo  9929  elfzom1p1elfzo  9942  ssfzo12  9952  ssfzo12bi  9953  fzofzp1b  9956  elfzonelfzo  9958  subfzo0  9970  qtri3or  9971  qletric  9972  qlelttric  9973  qltnle  9974  qdceq  9975  exbtwnzlemstep  9976  exbtwnzlemshrink  9977  exbtwnzlemex  9978  exbtwnz  9979  rebtwn2zlemstep  9981  rebtwn2z  9983  ioom  9989  ico0  9990  ioc0  9991  flltdivnn0lt  10028  flqeqceilz  10042  modqid2  10075  modqmuladd  10090  modqmuladdim  10091  modqmuladdnn0  10092  modqm1p1mod0  10099  modaddmodlo  10112  modfzo0difsn  10119  addmodlteq  10122  frec2uzuzd  10126  frec2uzltd  10127  frec2uzlt2d  10128  frec2uzrand  10129  frec2uzf1od  10130  frec2uzrdg  10133  frecuzrdgtcl  10136  frecuzrdgdomlem  10141  frecuzrdgfunlem  10143  frecfzennn  10150  uzennn  10160  uzsinds  10166  seq3clss  10191  iseqf1olemqf1o  10217  seq3f1olemp  10226  seq3id3  10231  seq3id  10232  seq3z  10235  ser3ge0  10241  expcl2lemap  10256  leexp2r  10298  leexp1a  10299  zesq  10361  expnbnd  10366  nn0opthlem2d  10418  nn0opthd  10419  facdiv  10435  facndiv  10436  facwordi  10437  faclbnd  10438  faclbnd6  10441  facubnd  10442  bcval4  10449  bcpasc  10463  bccl  10464  fiinfnf1o  10483  fihashf1rn  10486  hashunlem  10501  fiprsshashgt1  10514  hashfzo  10519  hashfzp1  10521  hashxp  10523  hashfacen  10530  zfz1iso  10535  seq3coll  10536  ovshftex  10542  reim0b  10585  cjap  10629  caucvgrelemcau  10703  caucvgre  10704  cvg1nlemres  10708  r19.29uz  10715  r19.2uz  10716  recvguniq  10718  sqrt0  10727  resqrexlemover  10733  resqrexlemdecn  10735  resqrexlemlo  10736  resqrexlemcalc3  10739  resqrexlemglsq  10745  resqrexlemga  10746  rsqrmo  10750  sqrtsq  10767  abs00ap  10785  absnid  10796  qabsor  10798  absexpzap  10803  abs3lem  10834  cau3lem  10837  caubnd2  10840  icodiamlt  10903  maxleim  10928  maxabslemlub  10930  maxabslemval  10931  fimaxre2  10949  negfi  10950  minmax  10952  xrmaxleim  10964  xrmaxiflemlub  10968  xrmaxiflemval  10970  xrminmax  10985  clim  11001  climuni  11013  climcn1  11028  climcn2  11029  mulcn2  11032  iserex  11059  climcau  11067  climcaucn  11071  sumrbdclem  11096  fsum3cvg  11097  summodclem2a  11101  zsumdc  11104  fsum3  11107  isumz  11109  fsumf1o  11110  fisumss  11112  fsum3cvg3  11116  fsumsplit  11127  fsum2dlemstep  11154  fsumconst  11174  modfsummod  11178  fsum00  11182  fsumabs  11185  fsumrelem  11191  fsumiun  11197  bcxmas  11209  isumsplit  11211  divcnv  11217  cvgratnnlemnexp  11244  cvgratnnlemmn  11245  mertenslem2  11256  efexp  11298  efieq1re  11387  eirrap  11391  dvdsval2  11403  moddvds  11409  dvds0  11415  absdvdsb  11418  dvdsabsb  11419  dvdsmul1  11422  dvdscmul  11427  dvdsmulc  11428  dvds2ln  11433  dvds2add  11434  dvds2sub  11435  dvdslelemd  11448  dvdsleabs2  11451  dvds1  11458  dvdsext  11460  fzo0dvdseq  11462  dvdsfac  11465  mulmoddvds  11468  odd2np1  11477  oddge22np1  11485  evennn02n  11486  evennn2n  11487  mulsucdiv2z  11489  sqoddm1div8z  11490  ltoddhalfle  11497  halfleoddlt  11498  m1expo  11504  nn0ehalf  11507  nn0o  11511  nn0oddm1d2  11513  nnoddm1d2  11514  divalglemeunn  11525  divalglemex  11526  divalglemeuneg  11527  flodddiv4  11538  zsupcllemstep  11545  dvdsbnd  11552  dvdslegcd  11560  gcdeq0  11572  gcd0id  11574  gcdneg  11577  gcdaddm  11579  gcdabs  11583  bezoutlemnewy  11591  bezoutlemstep  11592  bezoutlemzz  11597  bezoutlemaz  11598  bezoutlembz  11599  bezoutlembi  11600  bezoutlemeu  11602  bezoutlemle  11603  bezoutlemsup  11604  dvdsgcd  11607  dfgcd2  11609  rppwr  11623  dvdssqlem  11625  bezoutr1  11628  algfx  11640  eucalglt  11645  eucalgcvga  11646  lcmledvds  11658  lcmeq0  11659  lcmneg  11662  lcmabs  11664  lcmgcdlem  11665  lcmdvds  11667  lcmgcdeq  11671  coprmgcdb  11676  ncoprmgcdne1b  11677  coprmdvds  11680  qredeq  11684  qredeu  11685  rpdvds  11687  divgcdcoprm0  11689  divgcdcoprmex  11690  cncongr1  11691  cncongr2  11692  isprm2lem  11704  prmind2  11708  dvdsnprmd  11713  divgcdodd  11728  coprm  11729  isprm6  11732  prmfac1  11737  rpexp  11738  sqrt2irr  11747  pw2dvdseu  11752  sqrt2irrap  11764  nonsq  11791  hashdvds  11803  phimullem  11807  ennnfonelemk  11819  ennnfoneleminc  11830  ennnfonelemkh  11831  ennnfonelemhf1o  11832  ennnfonelemhom  11834  ennnfonelemrnh  11835  ennnfonelemdm  11839  ennnfone  11844  exmidunben  11845  ctinfom  11847  ctinf  11849  enctlem  11851  unct  11860  uniopn  12074  toponcomb  12101  bastg  12136  tgcl  12139  tgdom  12147  en1top  12152  tgss3  12153  bastop2  12159  epttop  12165  iuncld  12190  isopn3  12200  neiint  12220  neisspw  12223  0nnei  12228  neipsm  12229  opnneissb  12230  opnssneib  12231  tpnei  12235  neiuni  12236  opnneiid  12239  neissex  12240  ssrest  12257  tgcn  12283  tgcnp  12284  iscnp4  12293  cnpnei  12294  cnntr  12300  cnss1  12301  cnss2  12302  cncnp2m  12306  cnrest2  12311  cnrest2r  12312  cnptopresti  12313  cnptoprest2  12315  cndis  12316  lmss  12321  txcnp  12346  upxp  12347  txcn  12350  txdis1cn  12353  txlm  12354  hmeoopn  12386  hmeocld  12387  xblss2ps  12479  xblss2  12480  xblm  12492  blin2  12507  blbas  12508  xmeter  12511  isxms2  12527  metss  12569  metrest  12581  xmettxlem  12584  xmettx  12585  reopnap  12613  fsumcncntop  12631  rescncf  12643  cncfss  12645  cncfco  12653  cncfmptc  12657  mulcncflem  12665  mulcncf  12666  expcncf  12667  cnopnap  12669  dedekindeulemloc  12672  dedekindeulemlu  12674  dedekindeu  12676  suplociccreex  12677  dedekindicclemloc  12681  dedekindicclemlu  12683  dedekindicclemicc  12685  ivthinclemlr  12690  ivthinclemur  12692  ivthinclemloc  12694  ivthinc  12696  limcdifap  12706  limcimo  12709  cnplimcim  12711  cnplimccntop  12714  limccnp2lem  12720  dvfgg  12732  dvcnp2cntop  12738  dvcj  12748  dvexp  12750  dveflem  12761  dvef  12762  cbvrald  12829  uzdcinzz  12839  bdsepnft  12919  peano5set  12972  findset  12977  bj-omtrans  12988  bj-findis  13011  strcollnft  13016  pwtrufal  13026  exmid1stab  13029  subctctexmid  13030  peano4nninf  13034  nninfalllem1  13037  nninfall  13038  nninfsellemqall  13045  nninfomnilem  13048  nninffeq  13050  exmidsbthrlem  13051  exmidsbth  13053  sbthom  13055  isomninnlem  13059  trilpolemlt1  13068
  Copyright terms: Public domain W3C validator