ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ex Unicode 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  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
ex  |-  ( ph  ->  ( ps  ->  ch ) )

Proof of Theorem ex
StepHypRef Expression
1 ax-ia3 107 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
2 exp.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2syl6 33 1  |-  ( ph  ->  ( ps  ->  ch ) )
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  361  exp31  362  exp32  363  exp4b  365  exp41  368  exp43  370  exp53  375  impr  377  simplbi2  383  anidms  395  syl2anc  409  pm5.74da  440  imdistanda  445  pm5.32da  448  adantl4r  509  adantl5r  517  adantl6r  518  a2and  548  impbida  586  anim12dan  590  pm2.01da  626  pm2.65da  651  mtand  655  pm5.21im  686  jao  745  jaoian  785  jaodan  787  dcim  827  stdcn  833  impidc  844  pm2.5gdc  852  con1bidc  860  con2bidc  861  con1bdc  864  pm5.18dc  869  dfandc  870  pm4.63dc  872  pm4.54dc  888  pm5.21nd  902  dcan  919  dcor  920  annimdc  922  pm4.55dc  923  pm3.11dc  942  pm3.12dc  943  prlem1  958  pm3.2an3  1161  3jcad  1163  3impia  1179  3an1rs  1198  3exp1  1202  3exp2  1204  exp520  1207  syl3anl2  1266  3jaoian  1284  3jaodan  1285  mp3anl1  1310  mp3anl2  1311  mp3anl3  1312  inegd  1351  xor3dc  1366  pm5.15dc  1368  xor2dc  1369  xornbidc  1370  xordc  1371  nbbndc  1373  biassdc  1374  dfbi3dc  1376  pm5.24dc  1377  alanimi  1436  equsexd  1708  sbequ1  1742  sbiedv  1763  ax11v2  1793  equs5or  1803  sbequi  1812  exlimdd  1845  exlimddv  1871  cbvaldva  1901  cbvexdva  1902  nfsbxyt  1917  sbcomxyyz  1946  nfsb4t  1990  eupickbi  2082  moexexdc  2084  euexex  2085  2euswapdc  2091  dvelimdc  2302  nebidc  2389  rgen2a  2489  ralimiaa  2497  ralimdaa  2501  ralrimiva  2508  ralrimdva  2515  ralrimivva  2517  ralrimdvv  2519  ralrimdvva  2520  reximdva  2537  reximssdv  2539  reximddv2  2540  rexlimiva  2547  rexlimdva  2552  rexlimdvva  2560  r19.29vva  2580  2gencl  2722  vtocldf  2740  spcimdv  2773  spcimedv  2775  rspct  2785  eqvinc  2811  eqvincg  2812  ceqex  2815  reu6  2876  eqreu  2879  sbciedf  2947  rmob  3004  csbiebt  3043  csbiedf  3044  eqelssd  3120  reupick  3364  reximdva0m  3382  ssn0  3409  rgenm  3469  eqifdc  3510  preqr1g  3700  prel12  3705  dfnfc2  3761  intssunim  3800  intab  3807  iineq2d  3840  ssiun2  3863  mpteq2da  4024  exmid01  4128  pwntru  4129  exmid1dc  4130  exmidn0m  4131  exmidsssnc  4133  exmidundif  4136  exmidundifim  4137  copsexg  4173  copsex2t  4174  sess1  4266  sess2  4267  frirrg  4279  tron  4311  onelss  4316  onintss  4319  abnexg  4374  reusv1  4386  reusv3  4388  rabxfrd  4397  iunpw  4408  ssorduni  4410  ordsson  4415  ordsucg  4425  onintrab2im  4441  onsucelsucexmidlem  4451  elirr  4463  en2lp  4476  ordsuc  4485  ordpwsucss  4489  ordtri2or2exmid  4493  reg3exmidlemwe  4500  tfisi  4508  omsinds  4542  nnpredcl  4543  sosng  4619  2optocl  4623  relop  4696  releldmb  4783  relelrnb  4784  elrnmptg  4798  elreimasng  4912  relbrcnvg  4925  trin2  4937  ssxpbm  4981  ssxp1  4982  ssxp2  4983  elxp4  5033  elxp5  5034  relresfld  5075  relcoi1  5077  iotaval  5106  iotass  5112  funmo  5145  imadif  5210  imain  5212  2elresin  5241  feu  5312  fcnvres  5313  f0rn0  5324  f1oun  5394  f1oprg  5418  relfvssunirn  5444  funbrfv  5467  funbrfv2b  5473  dffn5im  5474  dfimafn  5477  funimass4  5479  ssimaex  5489  fvmptssdm  5512  fvmptf  5520  elfvmptrab1  5522  fvimacnv  5542  funimass3  5543  elpreima  5546  elrnrexdm  5566  eldmrexrn  5568  dffo4  5575  dffo5  5576  fmpt  5577  fmptdf  5584  ffvresb  5590  resflem  5591  fmptco  5593  fsn  5599  funfvima  5656  funfvima2  5657  f1mpt  5679  f1imass  5682  f1ocnvfvrneq  5690  foeqcnvco  5698  f1eqcocnv  5699  fliftfun  5704  fliftf  5707  isopolem  5730  isosolem  5732  eusvobj2  5767  acexmidlemab  5775  oprabid  5810  ovidi  5896  ovg  5916  suppssfv  5985  suppssov1  5986  funrnex  6019  f1dmex  6021  oprabexd  6032  fo2ndresm  6067  oprssdmm  6076  op1steq  6084  dfoprab3  6096  fo2ndf  6131  f1o2ndf1  6132  poxp  6136  spc2ed  6137  f1od2  6139  rbropapd  6146  reldmtpos  6157  rntpos  6161  tposf2  6172  tposf12  6173  issmo2  6193  smores  6196  smoiso  6206  tfrlem9  6223  tfrlemibacc  6230  tfrlemibfn  6232  tfrlemi14d  6237  tfrexlem  6238  tfr1onlembacc  6246  tfr1onlembfn  6248  tfr1onlemres  6253  tfri1dALT  6255  tfrcllembacc  6259  tfrcllembfn  6261  tfrcllemres  6266  tfrcl  6268  rdgivallem  6285  frecabcl  6303  frecrdg  6312  oawordi  6372  nnmcom  6392  nnsucelsuc  6394  nntri3or  6396  nnsucuniel  6398  nntri1  6399  nnsseleq  6404  nntr2  6406  dcdifsnid  6407  nnaordi  6411  nnmord  6420  nnaordex  6430  nnm00  6432  ertr  6451  erex  6460  iserd  6462  iinerm  6508  erinxp  6510  qsel  6513  qliftfun  6518  qliftfund  6519  2ecoptocl  6524  brecop  6526  mapss  6592  ixpssmap2g  6628  ixpssmapg  6629  dom2lem  6673  fundmen  6707  unen  6717  enm  6721  xpdom2  6732  fopwdom  6737  xpf1o  6745  mapen  6747  mapxpen  6749  ssenen  6752  phplem4  6756  nneneq  6758  snnen2og  6760  phplem4dom  6763  nndomo  6765  phpm  6766  phplem4on  6768  fidifsnen  6771  dif1enen  6781  fin0  6786  fin0or  6787  findcard2  6790  findcard2s  6791  findcard2d  6792  findcard2sd  6793  ac6sfi  6799  fimax2gtri  6802  finexdc  6803  en2eqpr  6808  onunsnss  6812  unfidisj  6817  undifdcss  6818  undifdc  6819  fiintim  6824  xpfi  6825  fisseneq  6827  ssfirab  6829  fnfi  6832  iunfidisj  6841  f1finf1o  6842  en1eqsnbi  6844  fidcenum  6851  isbth  6862  ssfii  6869  fieq0  6871  eqsupti  6890  suplub2ti  6895  isotilem  6900  supisoex  6903  eqinfti  6914  inflbti  6918  ordiso2  6927  djulclb  6947  updjudhf  6971  updjud  6974  difinfsn  6992  difinfinf  6993  ctmlemr  7000  ctm  7001  ctssdclemn0  7002  ctssdccl  7003  ctssdc  7005  enumct  7007  enomnilem  7017  finomni  7019  exmidomniim  7020  exmidomni  7021  fodjuomnilemdc  7023  fodjuomnilemres  7027  nnnninf  7030  ismkvnex  7036  mkvprop  7039  fodjumkvlemres  7040  enmkvlem  7042  enwomnilem  7049  pm54.43  7062  pr2nelem  7063  pr2ne  7064  exmidfodomrlemim  7073  exmidfodomrlemr  7074  exmidfodomrlemrALT  7075  acfun  7079  ccfunen  7095  cc1  7096  cc3  7099  cc4f  7100  cc4n  7102  mulcanpig  7166  nlt1pig  7172  addcmpblnq  7198  ltsonq  7229  ltexnqq  7239  prarloclemarch2  7250  enq0tr  7265  addcmpblnq0  7274  addnq0mo  7278  mulnq0mo  7279  prcdnql  7315  prcunqu  7316  prarloclemlo  7325  prarloclem3step  7327  prarloclem3  7328  genpdflem  7338  genpelvl  7343  genpelvu  7344  genpcdl  7350  genpcuu  7351  genprndl  7352  genprndu  7353  genpdisj  7354  addnqprllem  7358  addnqprulem  7359  addlocprlemeq  7364  addlocprlemgt  7365  nqprloc  7376  nqprl  7382  nqpru  7383  addnqprlemrl  7388  addnqprlemru  7389  addnqprlemfl  7390  addnqprlemfu  7391  prmuloc  7397  prmuloc2  7398  mullocpr  7402  mulnqprlemrl  7404  mulnqprlemru  7405  mulnqprlemfl  7406  mulnqprlemfu  7407  distrlem4prl  7415  distrlem4pru  7416  ltprordil  7420  1idprl  7421  1idpru  7422  ltpopr  7426  ltsopr  7427  ltaddpr  7428  ltexprlemm  7431  ltexprlemlol  7433  ltexprlemupu  7435  ltexprlemdisj  7437  ltexprlemloc  7438  ltexprlemrl  7441  ltexprlemru  7443  addcanprleml  7445  addcanprlemu  7446  addcanprg  7447  ltaprg  7450  recexprlemlol  7457  recexprlemdisj  7461  recexprlemloc  7462  recexprlem1ssl  7464  recexprlem1ssu  7465  aptiprleml  7470  aptiprlemu  7471  ltmprr  7473  archpr  7474  cauappcvgprlemm  7476  cauappcvgprlemopl  7477  cauappcvgprlemlol  7478  cauappcvgprlemopu  7479  cauappcvgprlemrnd  7481  cauappcvgprlemloc  7483  cauappcvgprlemladdfu  7485  cauappcvgprlemladdfl  7486  cauappcvgprlemladdru  7487  cauappcvgprlemladdrl  7488  caucvgprlemnkj  7497  caucvgprlemm  7499  caucvgprlemopl  7500  caucvgprlemlol  7501  caucvgprlemopu  7502  caucvgprlemrnd  7504  caucvgprlemloc  7506  caucvgprlemladdfu  7508  caucvgprlemladdrl  7509  caucvgprlemlim  7512  caucvgprprlemnkltj  7520  caucvgprprlemnkeqj  7521  caucvgprprlemnjltk  7522  caucvgprprlemml  7525  caucvgprprlemopl  7528  caucvgprprlemlol  7529  caucvgprprlemopu  7530  caucvgprprlemrnd  7532  caucvgprprlemloc  7534  caucvgprprlemexbt  7537  caucvgprprlemexb  7538  caucvgprprlemlim  7542  suplocexprlemrl  7548  suplocexprlemmu  7549  suplocexprlemru  7550  suplocexprlemloc  7552  suplocexprlemex  7553  suplocexprlemlub  7555  mulcmpblnrlemg  7571  addsrmo  7574  mulsrmo  7575  ltsrprg  7578  srpospr  7614  caucvgsrlemgt1  7626  map2psrprg  7636  suplocsrlemb  7637  suplocsrlempr  7638  suplocsrlem  7639  cnm  7663  pitonn  7679  nntopi  7725  axcaucvglemcau  7729  axcaucvglemres  7730  axpre-suploclemres  7732  lelttr  7875  ltletr  7876  readdcan  7925  cnegexlem1  7960  cnegexlem2  7961  addid0  8158  lelttrdi  8211  add20  8259  eqord1  8268  recexre  8363  inelr  8369  rimul  8370  apreap  8372  ltmul1  8377  cru  8387  apreim  8388  apirr  8390  apsym  8391  apcotr  8392  apadd1  8393  apneg  8396  mulext1  8397  msqge0  8401  mulge0  8404  apti  8407  ltleap  8417  aprcl  8431  recexap  8437  mulap0b  8439  mul0eqap  8454  recgt0  8631  prodgt02  8634  prodge02  8636  lemul12b  8642  lemul12a  8643  nnrecgt0  8781  addltmul  8979  nominpos  8980  elnnz  9087  peano2z  9113  zaddcllempos  9114  zaddcl  9117  zletric  9121  zlelttric  9122  zltnle  9123  zleloe  9124  zrevaddcl  9127  nzadd  9129  zdceq  9149  zdcle  9150  zdclt  9151  nn0n0n1ge2b  9153  nn0lt2  9155  zextle  9165  peano5uzti  9182  uzind2  9186  fzind  9189  fnn0ind  9190  nn0ind-raph  9191  btwnz  9193  eluzuzle  9357  uz11  9371  eluzp1m1  9372  supinfneg  9416  infsupneg  9417  lbzbi  9434  qapne  9457  qreccl  9460  qrevaddcl  9462  irradd  9464  irrmul  9465  elpq  9466  ledivge1le  9542  nn0ledivnn  9583  xrlelttr  9618  xrltletr  9619  npnflt  9627  nmnfgt  9630  xnn0lenn0nn0  9677  xnn0xadd0  9679  xleadd1  9687  xle2add  9691  xposdif  9694  xlesubadd  9695  ixxss1  9716  ixxss2  9717  ixxss12  9718  iccid  9737  elioc2  9748  elico2  9749  elicc2  9750  fznlem  9851  fzn  9852  fzen  9853  0fz1  9855  uzsubsubfz  9857  fzopth  9871  fzss1  9873  fzss2  9874  elfz1b  9900  uzsplit  9902  fzm1  9910  fznuz  9912  fzrevral  9915  elfz0ubfz0  9932  elfz0fzfz0  9933  fz0fzelfz0  9934  difelfzle  9941  1fv  9946  fzoss1  9978  fzosplit  9984  fzouzsplit  9986  fzonmapblen  9994  fzofzim  9995  eluzgtdifelfzo  10004  elfzodifsumelfzo  10008  elfzom1p1elfzo  10021  ssfzo12  10031  ssfzo12bi  10032  fzofzp1b  10035  elfzonelfzo  10037  subfzo0  10049  qtri3or  10050  qletric  10051  qlelttric  10052  qltnle  10053  qdceq  10054  exbtwnzlemstep  10055  exbtwnzlemshrink  10056  exbtwnzlemex  10057  exbtwnz  10058  rebtwn2zlemstep  10060  rebtwn2z  10062  ioom  10068  ico0  10069  ioc0  10070  flltdivnn0lt  10107  flqeqceilz  10121  modqid2  10154  modqmuladd  10169  modqmuladdim  10170  modqmuladdnn0  10171  modqm1p1mod0  10178  modaddmodlo  10191  modfzo0difsn  10198  addmodlteq  10201  frec2uzuzd  10205  frec2uzltd  10206  frec2uzlt2d  10207  frec2uzrand  10208  frec2uzf1od  10209  frec2uzrdg  10212  frecuzrdgtcl  10215  frecuzrdgdomlem  10220  frecuzrdgfunlem  10222  frecfzennn  10229  uzennn  10239  uzsinds  10245  seq3clss  10270  iseqf1olemqf1o  10296  seq3f1olemp  10305  seq3id3  10310  seq3id  10311  seq3z  10314  ser3ge0  10320  expcl2lemap  10335  leexp2r  10377  leexp1a  10378  zesq  10440  expnbnd  10445  nn0opthlem2d  10498  nn0opthd  10499  facdiv  10515  facndiv  10516  facwordi  10517  faclbnd  10518  faclbnd6  10521  facubnd  10522  bcval4  10529  bcpasc  10543  bccl  10544  fiinfnf1o  10563  fihashf1rn  10566  hashunlem  10581  fiprsshashgt1  10594  hashfzo  10599  hashfzp1  10601  hashxp  10603  hashfacen  10610  zfz1iso  10615  seq3coll  10616  ovshftex  10622  reim0b  10665  cjap  10709  caucvgrelemcau  10783  caucvgre  10784  cvg1nlemres  10788  r19.29uz  10795  r19.2uz  10796  recvguniq  10798  sqrt0  10807  resqrexlemover  10813  resqrexlemdecn  10815  resqrexlemlo  10816  resqrexlemcalc3  10819  resqrexlemglsq  10825  resqrexlemga  10826  rsqrmo  10830  sqrtsq  10847  abs00ap  10865  absnid  10876  qabsor  10878  absexpzap  10883  abs3lem  10914  cau3lem  10917  caubnd2  10920  icodiamlt  10983  maxleim  11008  maxabslemlub  11010  maxabslemval  11011  fimaxre2  11029  negfi  11030  minmax  11032  xrmaxleim  11044  xrmaxiflemlub  11048  xrmaxiflemval  11050  xrminmax  11065  clim  11081  climuni  11093  climcn1  11108  climcn2  11109  mulcn2  11112  iserex  11139  climcau  11147  climcaucn  11151  sumrbdclem  11177  fsum3cvg  11178  summodclem2a  11181  zsumdc  11184  fsum3  11187  isumz  11189  fsumf1o  11190  fisumss  11192  fsum3cvg3  11196  fsumsplit  11207  fsum2dlemstep  11234  fsumconst  11254  modfsummod  11258  fsum00  11262  fsumabs  11265  fsumrelem  11271  fsumiun  11277  bcxmas  11289  isumsplit  11291  divcnv  11297  cvgratnnlemnexp  11324  cvgratnnlemmn  11325  mertenslem2  11336  ntrivcvgap  11348  prodrbdclem  11371  prodmodclem2a  11376  prodmodc  11378  zproddc  11379  efexp  11423  efieq1re  11512  eirrap  11518  dvdsval2  11530  moddvds  11536  dvds0  11542  absdvdsb  11545  dvdsabsb  11546  dvdsmul1  11549  dvdscmul  11554  dvdsmulc  11555  dvds2ln  11560  dvds2add  11561  dvds2sub  11562  dvdslelemd  11575  dvdsleabs2  11578  dvds1  11585  dvdsext  11587  fzo0dvdseq  11589  dvdsfac  11592  mulmoddvds  11595  odd2np1  11604  oddge22np1  11612  evennn02n  11613  evennn2n  11614  mulsucdiv2z  11616  sqoddm1div8z  11617  ltoddhalfle  11624  halfleoddlt  11625  m1expo  11631  nn0ehalf  11634  nn0o  11638  nn0oddm1d2  11640  nnoddm1d2  11641  divalglemeunn  11652  divalglemex  11653  divalglemeuneg  11654  flodddiv4  11665  zsupcllemstep  11672  dvdsbnd  11679  dvdslegcd  11687  gcdeq0  11699  gcd0id  11701  gcdneg  11704  gcdaddm  11706  gcdabs  11710  bezoutlemnewy  11718  bezoutlemstep  11719  bezoutlemzz  11724  bezoutlemaz  11725  bezoutlembz  11726  bezoutlembi  11727  bezoutlemeu  11729  bezoutlemle  11730  bezoutlemsup  11731  dvdsgcd  11734  dfgcd2  11736  rppwr  11750  dvdssqlem  11752  bezoutr1  11755  algfx  11767  eucalglt  11772  eucalgcvga  11773  lcmledvds  11785  lcmeq0  11786  lcmneg  11789  lcmabs  11791  lcmgcdlem  11792  lcmdvds  11794  lcmgcdeq  11798  coprmgcdb  11803  ncoprmgcdne1b  11804  coprmdvds  11807  qredeq  11811  qredeu  11812  rpdvds  11814  divgcdcoprm0  11816  divgcdcoprmex  11817  cncongr1  11818  cncongr2  11819  isprm2lem  11831  prmind2  11835  dvdsnprmd  11840  divgcdodd  11855  coprm  11856  isprm6  11859  prmfac1  11864  rpexp  11865  sqrt2irr  11874  pw2dvdseu  11880  sqrt2irrap  11892  nonsq  11919  hashdvds  11931  phimullem  11935  ennnfonelemk  11947  ennnfoneleminc  11958  ennnfonelemkh  11959  ennnfonelemhf1o  11960  ennnfonelemhom  11962  ennnfonelemrnh  11963  ennnfonelemdm  11967  ennnfone  11972  exmidunben  11973  ctinfom  11975  ctinf  11977  enctlem  11979  unct  11989  omctfn  11990  uniopn  12205  toponcomb  12232  bastg  12267  tgcl  12270  tgdom  12278  en1top  12283  tgss3  12284  bastop2  12290  epttop  12296  iuncld  12321  isopn3  12331  neiint  12351  neisspw  12354  0nnei  12359  neipsm  12360  opnneissb  12361  opnssneib  12362  tpnei  12366  neiuni  12367  opnneiid  12370  neissex  12371  ssrest  12388  tgcn  12414  tgcnp  12415  iscnp4  12424  cnpnei  12425  cnntr  12431  cnss1  12432  cnss2  12433  cncnp2m  12437  cnrest2  12442  cnrest2r  12443  cnptopresti  12444  cnptoprest2  12446  cndis  12447  lmss  12452  txcnp  12477  upxp  12478  txcn  12481  txdis1cn  12484  txlm  12485  hmeoopn  12517  hmeocld  12518  xblss2ps  12610  xblss2  12611  xblm  12623  blin2  12638  blbas  12639  xmeter  12642  isxms2  12658  metss  12700  metrest  12712  xmettxlem  12715  xmettx  12716  reopnap  12744  fsumcncntop  12762  rescncf  12774  cncfss  12776  cncfco  12784  cncfmptc  12788  mulcncflem  12796  mulcncf  12797  expcncf  12798  cnopnap  12800  dedekindeulemloc  12803  dedekindeulemlu  12805  dedekindeu  12807  suplociccreex  12808  dedekindicclemloc  12812  dedekindicclemlu  12814  dedekindicclemicc  12816  ivthinclemlr  12821  ivthinclemur  12823  ivthinclemloc  12825  ivthinc  12827  limcdifap  12837  limcimo  12840  cnplimcim  12842  cnplimccntop  12845  limccnp2lem  12851  dvfgg  12863  dvcnp2cntop  12869  dvcj  12879  dvexp  12881  dveflem  12893  dvef  12894  eflt  12902  sin0pilem1  12908  coseq0q4123  12961  cos11  12980  logbgcd1irr  13090  logbgcd1irrap  13093  cbvrald  13164  uzdcinzz  13174  bdsepnft  13254  peano5set  13307  findset  13312  bj-omtrans  13323  bj-findis  13346  strcollnft  13351  pwtrufal  13363  exmid1stab  13366  subctctexmid  13367  peano4nninf  13373  nninfalllem1  13376  nninfall  13377  nninfsellemqall  13384  nninfomnilem  13387  nninffeq  13389  exmidsbthrlem  13390  exmidsbth  13392  sbthom  13394  isomninnlem  13398  trilpolemlt1  13407  apdiff  13414  ismkvnnlem  13417  neapmkvlem  13422
  Copyright terms: Public domain W3C validator