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

Proof of Theorem ex
StepHypRef Expression
1 ax-ia3 101 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
2 exp.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2syl6 29 1  |-  ( ph  ->  ( ps  ->  ch ) )
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  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  565  pm2.65da  587  mtand  591  pm5.21im  612  jao  672  jaoian  709  jaodan  710  impidc  755  pm2.5dc  763  con1bidc  768  con2bidc  769  con1bdc  772  pm5.18dc  777  dfandc  778  pm4.63dc  780  dcim  784  pm4.54dc  805  pm5.21nd  825  dcan  842  dcor  843  annimdc  845  pm4.55dc  846  pm3.11dc  864  pm3.12dc  865  prlem1  880  pm3.2an3  1083  3jcad  1085  3impia  1101  3an1rs  1116  3exp1  1120  3exp2  1122  exp520  1125  syl3anl2  1184  3jaoian  1200  3jaodan  1201  mp3anl1  1226  mp3anl2  1227  mp3anl3  1228  inegd  1263  xor3dc  1278  pm5.15dc  1280  xor2dc  1281  xornbidc  1282  xordc  1283  nbbndc  1285  biassdc  1286  dfbi3dc  1288  pm5.24dc  1289  alanimi  1348  equsexd  1617  sbequ1  1651  sbiedv  1672  ax11v2  1701  equs5or  1711  sbequi  1720  exlimdd  1752  exlimddv  1778  cbvaldva  1803  cbvexdva  1804  nfsbxyt  1819  sbcomxyyz  1846  nfsb4t  1890  eupickbi  1982  moexexdc  1984  euexex  1985  2euswapdc  1991  dvelimdc  2197  nebidc  2285  rgen2a  2375  ralimiaa  2383  ralimdaa  2386  ralrimiva  2392  ralrimdva  2399  ralrimivva  2401  ralrimdvv  2403  ralrimdvva  2404  reximdva  2421  rexlimiva  2428  rexlimdva  2433  rexlimdvva  2440  r19.29vva  2456  2gencl  2587  vtocldf  2605  spcimdv  2637  spcimedv  2639  rspct  2649  eqvinc  2667  eqvincg  2668  ceqex  2671  reu6  2730  eqreu  2733  sbciedf  2798  rmob  2850  csbiebt  2886  csbiedf  2887  reupick  3221  reximdva0m  3236  ssn0  3259  rgenm  3323  preqr1g  3537  prel12  3542  dfnfc2  3598  intssunim  3637  intab  3644  iineq2d  3677  ssiun2  3700  mpteq2da  3846  trintssm  3870  copsexg  3981  copsex2t  3982  sess1  4074  sess2  4075  frirrg  4087  tron  4119  onelss  4124  onintss  4127  reusv1  4190  reusv3  4192  rabxfrd  4201  iunpw  4211  ssorduni  4213  ordsson  4218  ordsucg  4228  onintrab2im  4244  onsucelsucexmidlem  4254  elirr  4266  en2lp  4278  ordsuc  4287  ordpwsucss  4291  ordtri2or2exmid  4296  reg3exmidlemwe  4303  tfisi  4310  sosng  4413  2optocl  4417  relop  4486  xpid11m  4557  releldmb  4571  relelrnb  4572  elrnmptg  4586  elreimasng  4691  relbrcnvg  4704  trin2  4716  ssxpbm  4756  ssxp1  4757  ssxp2  4758  elxp4  4808  elxp5  4809  relresfld  4847  relcoi1  4849  iotaval  4878  iotass  4884  funmo  4917  imadif  4979  imain  4981  2elresin  5010  feu  5072  fcnvres  5073  f1oun  5146  f1oprg  5168  relfvssunirn  5191  funbrfv  5212  funbrfv2b  5218  dffn5im  5219  dfimafn  5222  funimass4  5224  ssimaex  5234  fvmptssdm  5255  fvmptf  5263  fvimacnv  5282  funimass3  5283  elpreima  5286  elrnrexdm  5306  eldmrexrn  5308  dffo4  5315  dffo5  5316  fmpt  5319  ffvresb  5328  fmptco  5330  fsn  5335  funfvima  5390  funfvima2  5391  f1mpt  5410  f1imass  5413  f1ocnvfvrneq  5422  foeqcnvco  5430  f1eqcocnv  5431  fliftfun  5436  fliftf  5439  isopolem  5461  isosolem  5463  eusvobj2  5498  acexmidlemab  5506  oprabid  5537  ovidi  5619  ovg  5639  suppssfv  5708  suppssov1  5709  funrnex  5741  f1dmex  5743  oprabexd  5754  fo2ndresm  5789  op1steq  5805  dfoprab3  5817  fo2ndf  5848  f1o2ndf1  5849  poxp  5853  isprmpt2  5858  reldmtpos  5868  rntpos  5872  tposf2  5883  tposf12  5884  issmo2  5904  smores  5907  smoiso  5917  tfrlem9  5935  tfrlemibacc  5940  tfrlemibfn  5942  tfrlemi14d  5947  tfrexlem  5948  rdgivallem  5968  frecsuclem3  5990  frecrdg  5992  freccl  5993  oawordi  6049  nnmcom  6068  nnsucelsuc  6070  nntri3or  6072  nntri1  6074  nnsseleq  6079  nndifsnid  6080  nnaordi  6081  nnmord  6090  nnaordex  6100  nnm00  6102  ertr  6121  erex  6130  iserd  6132  iinerm  6178  erinxp  6180  qsel  6183  qliftfun  6188  qliftfund  6189  2ecoptocl  6194  brecop  6196  dom2lem  6252  fundmen  6286  unen  6293  enm  6294  xpdom2  6305  fopwdom  6310  phplem4  6318  nneneq  6320  snnen2og  6322  phplem4dom  6324  nndomo  6326  phpm  6327  phplem4on  6329  fidifsnen  6331  fidifsnid  6332  fin0  6342  fin0or  6343  findcard2  6346  findcard2s  6347  findcard2d  6348  findcard2sd  6349  ac6sfi  6352  onunsnss  6355  ordiso2  6357  mulcanpig  6433  nlt1pig  6439  addcmpblnq  6465  ltsonq  6496  ltexnqq  6506  prarloclemarch2  6517  enq0tr  6532  addcmpblnq0  6541  addnq0mo  6545  mulnq0mo  6546  prcdnql  6582  prcunqu  6583  prarloclemlo  6592  prarloclem3step  6594  prarloclem3  6595  genpdflem  6605  genpelvl  6610  genpelvu  6611  genpcdl  6617  genpcuu  6618  genprndl  6619  genprndu  6620  genpdisj  6621  addnqprllem  6625  addnqprulem  6626  addlocprlemeq  6631  addlocprlemgt  6632  nqprloc  6643  nqprl  6649  nqpru  6650  addnqprlemrl  6655  addnqprlemru  6656  addnqprlemfl  6657  addnqprlemfu  6658  prmuloc  6664  prmuloc2  6665  mullocpr  6669  mulnqprlemrl  6671  mulnqprlemru  6672  mulnqprlemfl  6673  mulnqprlemfu  6674  distrlem4prl  6682  distrlem4pru  6683  ltprordil  6687  1idprl  6688  1idpru  6689  ltpopr  6693  ltsopr  6694  ltaddpr  6695  ltexprlemm  6698  ltexprlemlol  6700  ltexprlemupu  6702  ltexprlemdisj  6704  ltexprlemloc  6705  ltexprlemrl  6708  ltexprlemru  6710  addcanprleml  6712  addcanprlemu  6713  addcanprg  6714  ltaprg  6717  recexprlemlol  6724  recexprlemdisj  6728  recexprlemloc  6729  recexprlem1ssl  6731  recexprlem1ssu  6732  aptiprleml  6737  aptiprlemu  6738  ltmprr  6740  archpr  6741  cauappcvgprlemm  6743  cauappcvgprlemopl  6744  cauappcvgprlemlol  6745  cauappcvgprlemopu  6746  cauappcvgprlemrnd  6748  cauappcvgprlemloc  6750  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgprlemnkj  6764  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemlol  6768  caucvgprlemopu  6769  caucvgprlemrnd  6771  caucvgprlemloc  6773  caucvgprlemladdfu  6775  caucvgprlemladdrl  6776  caucvgprlemlim  6779  caucvgprprlemnkltj  6787  caucvgprprlemnkeqj  6788  caucvgprprlemnjltk  6789  caucvgprprlemml  6792  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemopu  6797  caucvgprprlemrnd  6799  caucvgprprlemloc  6801  caucvgprprlemexbt  6804  caucvgprprlemexb  6805  caucvgprprlemlim  6809  mulcmpblnrlemg  6825  addsrmo  6828  mulsrmo  6829  ltsrprg  6832  srpospr  6867  caucvgsrlemgt1  6879  pitonn  6924  nntopi  6968  axcaucvglemcau  6972  axcaucvglemres  6973  lelttr  7106  ltletr  7107  readdcan  7153  cnegexlem1  7186  cnegexlem2  7187  lelttrdi  7421  add20  7469  recexre  7569  inelr  7575  rimul  7576  apreap  7578  ltmul1  7583  cru  7593  apreim  7594  apirr  7596  apsym  7597  apcotr  7598  apadd1  7599  apneg  7602  mulext1  7603  msqge0  7607  mulge0  7610  apti  7613  ltleap  7621  recexap  7634  mulap0b  7636  recgt0  7816  prodgt02  7819  prodge02  7821  lemul12b  7827  lemul12a  7828  nnrecgt0  7951  addltmul  8161  nominpos  8162  elnnz  8255  peano2z  8281  zaddcllempos  8282  zaddcl  8285  zletric  8289  zlelttric  8290  zltnle  8291  zleloe  8292  zrevaddcl  8295  zdceq  8316  zdcle  8317  zdclt  8318  nn0n0n1ge2b  8320  nn0lt2  8322  zextle  8331  peano5uzti  8346  uzind2  8350  fzind  8353  fnn0ind  8354  nn0ind-raph  8355  btwnz  8357  eluzuzle  8481  uz11  8495  eluzp1m1  8496  lbzbi  8551  qapne  8574  qreccl  8576  qrevaddcl  8578  irradd  8580  irrmul  8581  ledivge1le  8652  xrlelttr  8722  xrltletr  8723  ixxss1  8773  ixxss2  8774  ixxss12  8775  iccid  8794  elioc2  8805  elico2  8806  elicc2  8807  fznlem  8905  fzn  8906  fzen  8907  0fz1  8909  uzsubsubfz  8911  fzopth  8924  fzss1  8926  fzss2  8927  elfz1b  8952  uzsplit  8954  fzm1  8962  fznuz  8964  fzrevral  8967  elfz0ubfz0  8982  elfz0fzfz0  8983  fz0fzelfz0  8984  difelfzle  8992  1fv  8996  fzoss1  9027  fzosplit  9033  fzouzsplit  9035  fzonmapblen  9043  fzofzim  9044  eluzgtdifelfzo  9053  elfzodifsumelfzo  9057  elfzom1p1elfzo  9070  ssfzo12  9080  ssfzo12bi  9081  fzofzp1b  9084  elfzonelfzo  9086  subfzo0  9097  qtri3or  9098  qletric  9099  qlelttric  9100  qltnle  9101  qdceq  9102  qbtwnzlemstep  9103  qbtwnzlemex  9105  qbtwnz  9106  rebtwn2zlemstep  9107  rebtwn2z  9109  flltdivnn0lt  9146  flqeqceilz  9160  frec2uzzd  9186  frec2uzuzd  9188  frec2uzltd  9189  frec2uzlt2d  9190  frec2uzrand  9191  frec2uzf1od  9192  frec2uzrdg  9195  frecuzrdgfn  9198  frecfzennn  9203  iseqid3s  9246  iseqid  9247  expival  9257  expcl2lemap  9267  leexp2r  9308  leexp1a  9309  zesq  9367  expnbnd  9372  ovshftex  9420  reim0b  9462  cjap  9506  caucvgrelemcau  9579  caucvgre  9580  cvg1nlemres  9584  r19.29uz  9590  r19.2uz  9591  recvguniq  9593  sqrt0  9602  resqrexlemover  9608  resqrexlemdecn  9610  resqrexlemlo  9611  resqrexlemcalc3  9614  resqrexlemglsq  9620  resqrexlemga  9621  rsqrmo  9625  sqrtsq  9642  abs00ap  9660  absnid  9671  absexpzap  9676  abs3lem  9707  cau3lem  9710  caubnd2  9713  icodiamlt  9776  clim  9802  climuni  9814  climcn1  9829  climcn2  9830  mulcn2  9833  iiserex  9859  climcau  9866  climcaucn  9870  sqrt2irr  9878  ialgfx  9891  cbvrald  9927  bdsepnft  10007  peano5set  10064  peano5setOLD  10065  findset  10070  bj-omtrans  10081  bj-findis  10104  strcollnft  10109
  Copyright terms: Public domain W3C validator