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  789  pm2.5dc  797  con1bidc  802  con2bidc  803  con1bdc  806  pm5.18dc  811  dfandc  812  pm4.63dc  814  dcim  818  pm4.54dc  839  pm5.21nd  859  dcan  876  dcor  877  annimdc  879  pm4.55dc  880  pm3.11dc  899  pm3.12dc  900  prlem1  915  pm3.2an3  1118  3jcad  1120  3impia  1136  3an1rs  1151  3exp1  1155  3exp2  1157  exp520  1160  syl3anl2  1219  3jaoian  1237  3jaodan  1238  mp3anl1  1263  mp3anl2  1264  mp3anl3  1265  inegd  1304  xor3dc  1319  pm5.15dc  1321  xor2dc  1322  xornbidc  1323  xordc  1324  nbbndc  1326  biassdc  1327  dfbi3dc  1329  pm5.24dc  1330  alanimi  1389  equsexd  1658  sbequ1  1692  sbiedv  1713  ax11v2  1742  equs5or  1752  sbequi  1761  exlimdd  1794  exlimddv  1820  cbvaldva  1845  cbvexdva  1846  nfsbxyt  1861  sbcomxyyz  1888  nfsb4t  1932  eupickbi  2024  moexexdc  2026  euexex  2027  2euswapdc  2033  dvelimdc  2239  nebidc  2326  rgen2a  2418  ralimiaa  2426  ralimdaa  2429  ralrimiva  2435  ralrimdva  2442  ralrimivva  2444  ralrimdvv  2446  ralrimdvva  2447  reximdva  2464  reximddv2  2466  rexlimiva  2473  rexlimdva  2478  rexlimdvva  2485  r19.29vva  2501  2gencl  2633  vtocldf  2651  spcimdv  2683  spcimedv  2685  rspct  2695  eqvinc  2719  eqvincg  2720  ceqex  2723  reu6  2782  eqreu  2785  sbciedf  2850  rmob  2907  csbiebt  2943  csbiedf  2944  reupick  3255  reximdva0m  3270  ssn0  3293  rgenm  3351  preqr1g  3566  prel12  3571  dfnfc2  3627  intssunim  3666  intab  3673  iineq2d  3706  ssiun2  3729  mpteq2da  3875  trintssmOLD  3900  copsexg  4007  copsex2t  4008  sess1  4100  sess2  4101  frirrg  4113  tron  4145  onelss  4150  onintss  4153  reusv1  4216  reusv3  4218  rabxfrd  4227  iunpw  4237  ssorduni  4239  ordsson  4244  ordsucg  4254  onintrab2im  4270  onsucelsucexmidlem  4280  elirr  4292  en2lp  4305  ordsuc  4314  ordpwsucss  4318  ordtri2or2exmid  4322  reg3exmidlemwe  4329  tfisi  4336  sosng  4439  2optocl  4443  relop  4514  xpid11m  4585  releldmb  4599  relelrnb  4600  elrnmptg  4614  elreimasng  4721  relbrcnvg  4734  trin2  4746  ssxpbm  4786  ssxp1  4787  ssxp2  4788  elxp4  4838  elxp5  4839  relresfld  4877  relcoi1  4879  iotaval  4908  iotass  4914  funmo  4947  imadif  5010  imain  5012  2elresin  5041  feu  5103  fcnvres  5104  f1oun  5177  f1oprg  5199  relfvssunirn  5222  funbrfv  5244  funbrfv2b  5250  dffn5im  5251  dfimafn  5254  funimass4  5256  ssimaex  5266  fvmptssdm  5287  fvmptf  5295  fvimacnv  5314  funimass3  5315  elpreima  5318  elrnrexdm  5338  eldmrexrn  5340  dffo4  5347  dffo5  5348  fmpt  5351  ffvresb  5360  fmptco  5362  fsn  5367  funfvima  5422  funfvima2  5423  f1mpt  5442  f1imass  5445  f1ocnvfvrneq  5453  foeqcnvco  5461  f1eqcocnv  5462  fliftfun  5467  fliftf  5470  isopolem  5492  isosolem  5494  eusvobj2  5529  acexmidlemab  5537  oprabid  5568  ovidi  5650  ovg  5670  suppssfv  5739  suppssov1  5740  funrnex  5772  f1dmex  5774  oprabexd  5785  fo2ndresm  5820  op1steq  5836  dfoprab3  5848  fo2ndf  5879  f1o2ndf1  5880  poxp  5884  spc2ed  5885  f1od2  5887  isprmpt2  5892  reldmtpos  5902  rntpos  5906  tposf2  5917  tposf12  5918  issmo2  5938  smores  5941  smoiso  5951  tfrlem9  5968  tfrlemibacc  5975  tfrlemibfn  5977  tfrlemi14d  5982  tfrexlem  5983  tfr1onlembacc  5991  tfr1onlembfn  5993  tfr1onlemres  5998  tfri1dALT  6000  tfrcllembacc  6004  tfrcllembfn  6006  tfrcllemres  6011  tfrcl  6013  rdgivallem  6030  frecabcl  6048  frecrdg  6057  oawordi  6113  nnmcom  6133  nnsucelsuc  6135  nntri3or  6137  nnsucuniel  6139  nntri1  6140  nnsseleq  6145  nndifsnid  6146  nnaordi  6147  nnmord  6156  nnaordex  6166  nnm00  6168  ertr  6187  erex  6196  iserd  6198  iinerm  6244  erinxp  6246  qsel  6249  qliftfun  6254  qliftfund  6255  2ecoptocl  6260  brecop  6262  dom2lem  6319  fundmen  6353  unen  6361  enm  6364  xpdom2  6375  fopwdom  6380  xpf1o  6385  phplem4  6390  nneneq  6392  snnen2og  6394  phplem4dom  6397  nndomo  6399  phpm  6400  phplem4on  6402  fidifsnen  6405  fidifsnid  6406  fin0  6419  fin0or  6420  findcard2  6423  findcard2s  6424  findcard2d  6425  findcard2sd  6426  ac6sfi  6431  en2eqpr  6434  onunsnss  6437  unfidisj  6442  undiffi  6443  fnfi  6446  eqsupti  6468  suplub2ti  6473  isotilem  6478  supisoex  6481  eqinfti  6492  inflbti  6496  ordiso2  6505  pm54.43  6518  pr2nelem  6519  pr2ne  6520  mulcanpig  6587  nlt1pig  6593  addcmpblnq  6619  ltsonq  6650  ltexnqq  6660  prarloclemarch2  6671  enq0tr  6686  addcmpblnq0  6695  addnq0mo  6699  mulnq0mo  6700  prcdnql  6736  prcunqu  6737  prarloclemlo  6746  prarloclem3step  6748  prarloclem3  6749  genpdflem  6759  genpelvl  6764  genpelvu  6765  genpcdl  6771  genpcuu  6772  genprndl  6773  genprndu  6774  genpdisj  6775  addnqprllem  6779  addnqprulem  6780  addlocprlemeq  6785  addlocprlemgt  6786  nqprloc  6797  nqprl  6803  nqpru  6804  addnqprlemrl  6809  addnqprlemru  6810  addnqprlemfl  6811  addnqprlemfu  6812  prmuloc  6818  prmuloc2  6819  mullocpr  6823  mulnqprlemrl  6825  mulnqprlemru  6826  mulnqprlemfl  6827  mulnqprlemfu  6828  distrlem4prl  6836  distrlem4pru  6837  ltprordil  6841  1idprl  6842  1idpru  6843  ltpopr  6847  ltsopr  6848  ltaddpr  6849  ltexprlemm  6852  ltexprlemlol  6854  ltexprlemupu  6856  ltexprlemdisj  6858  ltexprlemloc  6859  ltexprlemrl  6862  ltexprlemru  6864  addcanprleml  6866  addcanprlemu  6867  addcanprg  6868  ltaprg  6871  recexprlemlol  6878  recexprlemdisj  6882  recexprlemloc  6883  recexprlem1ssl  6885  recexprlem1ssu  6886  aptiprleml  6891  aptiprlemu  6892  ltmprr  6894  archpr  6895  cauappcvgprlemm  6897  cauappcvgprlemopl  6898  cauappcvgprlemlol  6899  cauappcvgprlemopu  6900  cauappcvgprlemrnd  6902  cauappcvgprlemloc  6904  cauappcvgprlemladdfu  6906  cauappcvgprlemladdfl  6907  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  caucvgprlemnkj  6918  caucvgprlemm  6920  caucvgprlemopl  6921  caucvgprlemlol  6922  caucvgprlemopu  6923  caucvgprlemrnd  6925  caucvgprlemloc  6927  caucvgprlemladdfu  6929  caucvgprlemladdrl  6930  caucvgprlemlim  6933  caucvgprprlemnkltj  6941  caucvgprprlemnkeqj  6942  caucvgprprlemnjltk  6943  caucvgprprlemml  6946  caucvgprprlemopl  6949  caucvgprprlemlol  6950  caucvgprprlemopu  6951  caucvgprprlemrnd  6953  caucvgprprlemloc  6955  caucvgprprlemexbt  6958  caucvgprprlemexb  6959  caucvgprprlemlim  6963  mulcmpblnrlemg  6979  addsrmo  6982  mulsrmo  6983  ltsrprg  6986  srpospr  7021  caucvgsrlemgt1  7033  pitonn  7078  nntopi  7122  axcaucvglemcau  7126  axcaucvglemres  7127  lelttr  7266  ltletr  7267  readdcan  7315  cnegexlem1  7350  cnegexlem2  7351  addid0  7544  lelttrdi  7597  add20  7645  recexre  7745  inelr  7751  rimul  7752  apreap  7754  ltmul1  7759  cru  7769  apreim  7770  apirr  7772  apsym  7773  apcotr  7774  apadd1  7775  apneg  7778  mulext1  7779  msqge0  7783  mulge0  7786  apti  7789  ltleap  7797  recexap  7810  mulap0b  7812  recgt0  7995  prodgt02  7998  prodge02  8000  lemul12b  8006  lemul12a  8007  nnrecgt0  8143  addltmul  8334  nominpos  8335  elnnz  8442  peano2z  8468  zaddcllempos  8469  zaddcl  8472  zletric  8476  zlelttric  8477  zltnle  8478  zleloe  8479  zrevaddcl  8482  nzadd  8484  zdceq  8504  zdcle  8505  zdclt  8506  nn0n0n1ge2b  8508  nn0lt2  8510  zextle  8519  peano5uzti  8536  uzind2  8540  fzind  8543  fnn0ind  8544  nn0ind-raph  8545  btwnz  8547  eluzuzle  8708  uz11  8722  eluzp1m1  8723  supinfneg  8764  infsupneg  8765  lbzbi  8782  qapne  8805  qreccl  8808  qrevaddcl  8810  irradd  8812  irrmul  8813  ledivge1le  8884  nn0ledivnn  8919  xrlelttr  8952  xrltletr  8953  ixxss1  9003  ixxss2  9004  ixxss12  9005  iccid  9024  elioc2  9035  elico2  9036  elicc2  9037  fznlem  9136  fzn  9137  fzen  9138  0fz1  9140  uzsubsubfz  9142  fzopth  9155  fzss1  9157  fzss2  9158  elfz1b  9183  uzsplit  9185  fzm1  9193  fznuz  9195  fzrevral  9198  elfz0ubfz0  9213  elfz0fzfz0  9214  fz0fzelfz0  9215  difelfzle  9222  1fv  9226  fzoss1  9257  fzosplit  9263  fzouzsplit  9265  fzonmapblen  9273  fzofzim  9274  eluzgtdifelfzo  9283  elfzodifsumelfzo  9287  elfzom1p1elfzo  9300  ssfzo12  9310  ssfzo12bi  9311  fzofzp1b  9314  elfzonelfzo  9316  subfzo0  9328  qtri3or  9329  qletric  9330  qlelttric  9331  qltnle  9332  qdceq  9333  exbtwnzlemstep  9334  exbtwnzlemshrink  9335  exbtwnzlemex  9336  exbtwnz  9337  rebtwn2zlemstep  9339  rebtwn2z  9341  ioom  9347  ico0  9348  ioc0  9349  flltdivnn0lt  9386  flqeqceilz  9400  modqid2  9433  modqmuladd  9448  modqmuladdim  9449  modqmuladdnn0  9450  modqm1p1mod0  9457  modaddmodlo  9470  modfzo0difsn  9477  addmodlteq  9480  frec2uzuzd  9484  frec2uzltd  9485  frec2uzlt2d  9486  frec2uzrand  9487  frec2uzf1od  9488  frec2uzrdg  9491  frecuzrdgtcl  9494  frecuzrdgdomlem  9499  frecuzrdgfunlem  9501  frecfzennn  9508  uzsinds  9518  iseqoveq  9540  iseqid3s  9562  iseqid  9563  iseqz  9566  expival  9575  expcl2lemap  9585  leexp2r  9627  leexp1a  9628  zesq  9688  expnbnd  9693  nn0opthlem2d  9745  nn0opthd  9746  facdiv  9762  facndiv  9763  facwordi  9764  faclbnd  9765  faclbnd6  9768  facubnd  9769  bcval4  9776  bcpasc  9790  bccl  9791  fiinfnf1o  9810  sizef1rn  9813  sizeunlem  9828  ovshftex  9845  reim0b  9887  cjap  9931  caucvgrelemcau  10004  caucvgre  10005  cvg1nlemres  10009  r19.29uz  10016  r19.2uz  10017  recvguniq  10019  sqrt0  10028  resqrexlemover  10034  resqrexlemdecn  10036  resqrexlemlo  10037  resqrexlemcalc3  10040  resqrexlemglsq  10046  resqrexlemga  10047  rsqrmo  10051  sqrtsq  10068  abs00ap  10086  absnid  10097  qabsor  10099  absexpzap  10104  abs3lem  10135  cau3lem  10138  caubnd2  10141  icodiamlt  10204  maxleim  10229  maxabslemlub  10231  maxabslemval  10232  fimaxre2  10247  negfi  10248  minmax  10250  clim  10258  climuni  10270  climcn1  10285  climcn2  10286  mulcn2  10289  iiserex  10315  climcau  10322  climcaucn  10326  isumrblem  10337  fisumcvg  10338  dvdsval2  10343  moddvds  10349  dvds0  10355  absdvdsb  10358  dvdsabsb  10359  dvdsmul1  10362  dvdscmul  10367  dvdsmulc  10368  dvds2ln  10373  dvds2add  10374  dvds2sub  10375  dvdslelemd  10388  dvdsleabs2  10391  dvds1  10398  dvdsext  10400  fzo0dvdseq  10402  dvdsfac  10405  mulmoddvds  10408  odd2np1  10417  oddge22np1  10425  evennn02n  10426  evennn2n  10427  mulsucdiv2z  10429  sqoddm1div8z  10430  ltoddhalfle  10437  halfleoddlt  10438  m1expo  10444  nn0ehalf  10447  nn0o  10451  nn0oddm1d2  10453  nnoddm1d2  10454  divalglemeunn  10465  divalglemex  10466  divalglemeuneg  10467  flodddiv4  10478  zsupcllemstep  10485  dvdsbnd  10492  dvdslegcd  10500  gcdeq0  10512  gcd0id  10514  gcdneg  10517  gcdaddm  10519  gcdabs  10523  bezoutlemnewy  10529  bezoutlemstep  10530  bezoutlemzz  10535  bezoutlemaz  10536  bezoutlembz  10537  bezoutlembi  10538  bezoutlemeu  10540  bezoutlemle  10541  bezoutlemsup  10542  dvdsgcd  10545  dfgcd2  10547  rppwr  10561  dvdssqlem  10563  bezoutr1  10566  ialgfx  10578  eucalglt  10583  eucialgcvga  10584  lcmledvds  10596  lcmeq0  10597  lcmneg  10600  lcmabs  10602  lcmgcdlem  10603  lcmdvds  10605  lcmgcdeq  10609  coprmgcdb  10614  ncoprmgcdne1b  10615  coprmdvds  10618  qredeq  10622  qredeu  10623  rpdvds  10625  divgcdcoprm0  10627  divgcdcoprmex  10628  cncongr1  10629  cncongr2  10630  isprm2lem  10642  prmind2  10646  dvdsnprmd  10651  divgcdodd  10666  coprm  10667  isprm6  10670  prmfac1  10675  rpexp  10676  sqrt2irr  10685  pw2dvdseu  10690  sqrt2irrap  10702  cbvrald  10749  uzdcinzz  10759  bdsepnft  10836  peano5set  10893  findset  10898  bj-omtrans  10909  bj-findis  10932  strcollnft  10937
  Copyright terms: Public domain W3C validator