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

Proof of Theorem ex
StepHypRef Expression
1 ax-ia3 106 . 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 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  3595  prel12  3600  dfnfc2  3656  intssunim  3695  intab  3702  iineq2d  3735  ssiun2  3758  mpteq2da  3904  trintssmOLD  3930  exmid01  4008  exmidundif  4011  copsexg  4047  copsex2t  4048  sess1  4140  sess2  4141  frirrg  4153  tron  4185  onelss  4190  onintss  4193  reusv1  4256  reusv3  4258  rabxfrd  4267  iunpw  4277  ssorduni  4279  ordsson  4284  ordsucg  4294  onintrab2im  4310  onsucelsucexmidlem  4320  elirr  4332  en2lp  4345  ordsuc  4354  ordpwsucss  4358  ordtri2or2exmid  4362  reg3exmidlemwe  4369  tfisi  4377  omsinds  4410  sosng  4481  2optocl  4485  relop  4556  xpid11m  4628  releldmb  4642  relelrnb  4643  elrnmptg  4657  elreimasng  4767  relbrcnvg  4780  trin2  4792  ssxpbm  4834  ssxp1  4835  ssxp2  4836  elxp4  4886  elxp5  4887  relresfld  4928  relcoi1  4930  iotaval  4959  iotass  4965  funmo  4998  imadif  5061  imain  5063  2elresin  5092  feu  5158  fcnvres  5159  f0rn0  5170  f1oun  5238  f1oprg  5260  relfvssunirn  5286  funbrfv  5308  funbrfv2b  5314  dffn5im  5315  dfimafn  5318  funimass4  5320  ssimaex  5330  fvmptssdm  5352  fvmptf  5360  fvimacnv  5379  funimass3  5380  elpreima  5383  elrnrexdm  5403  eldmrexrn  5405  dffo4  5412  dffo5  5413  fmpt  5414  fmptdf  5420  ffvresb  5426  resflem  5427  fmptco  5429  fsn  5434  funfvima  5489  funfvima2  5490  f1mpt  5513  f1imass  5516  f1ocnvfvrneq  5524  foeqcnvco  5532  f1eqcocnv  5533  fliftfun  5538  fliftf  5541  isopolem  5564  isosolem  5566  eusvobj2  5601  acexmidlemab  5609  oprabid  5640  ovidi  5722  ovg  5742  suppssfv  5811  suppssov1  5812  funrnex  5844  f1dmex  5846  oprabexd  5857  fo2ndresm  5892  op1steq  5908  dfoprab3  5920  fo2ndf  5951  f1o2ndf1  5952  poxp  5956  spc2ed  5957  f1od2  5959  isprmpt2  5964  reldmtpos  5974  rntpos  5978  tposf2  5989  tposf12  5990  issmo2  6010  smores  6013  smoiso  6023  tfrlem9  6040  tfrlemibacc  6047  tfrlemibfn  6049  tfrlemi14d  6054  tfrexlem  6055  tfr1onlembacc  6063  tfr1onlembfn  6065  tfr1onlemres  6070  tfri1dALT  6072  tfrcllembacc  6076  tfrcllembfn  6078  tfrcllemres  6083  tfrcl  6085  rdgivallem  6102  frecabcl  6120  frecrdg  6129  oawordi  6186  nnmcom  6206  nnsucelsuc  6208  nntri3or  6210  nnsucuniel  6212  nntri1  6213  nnsseleq  6218  dcdifsnid  6219  nnaordi  6221  nnmord  6230  nnaordex  6240  nnm00  6242  ertr  6261  erex  6270  iserd  6272  iinerm  6318  erinxp  6320  qsel  6323  qliftfun  6328  qliftfund  6329  2ecoptocl  6334  brecop  6336  mapss  6402  dom2lem  6443  fundmen  6477  unen  6487  enm  6490  xpdom2  6501  fopwdom  6506  xpf1o  6514  mapen  6516  mapxpen  6518  ssenen  6521  phplem4  6525  nneneq  6527  snnen2og  6529  phplem4dom  6532  nndomo  6534  phpm  6535  phplem4on  6537  fidifsnen  6540  dif1enen  6550  fin0  6555  fin0or  6556  findcard2  6559  findcard2s  6560  findcard2d  6561  findcard2sd  6562  ac6sfi  6568  fimax2gtri  6571  finexdc  6572  en2eqpr  6577  onunsnss  6581  unfidisj  6586  undifdcss  6587  undifdc  6588  xpfi  6593  fisseneq  6595  ssfirab  6596  fnfi  6599  f1finf1o  6608  en1eqsnbi  6610  isbth  6623  eqsupti  6638  suplub2ti  6643  isotilem  6648  supisoex  6651  eqinfti  6662  inflbti  6666  ordiso2  6675  djulclb  6694  updjudhf  6717  updjud  6720  enomnilem  6741  finomni  6743  exmidomniim  6744  exmidomni  6745  fodjuomnilemdc  6746  fodjuomnilemres  6750  nnnninf  6753  pm54.43  6765  pr2nelem  6766  pr2ne  6767  exmidfodomrlemim  6774  exmidfodomrlemr  6775  exmidfodomrlemrALT  6776  mulcanpig  6841  nlt1pig  6847  addcmpblnq  6873  ltsonq  6904  ltexnqq  6914  prarloclemarch2  6925  enq0tr  6940  addcmpblnq0  6949  addnq0mo  6953  mulnq0mo  6954  prcdnql  6990  prcunqu  6991  prarloclemlo  7000  prarloclem3step  7002  prarloclem3  7003  genpdflem  7013  genpelvl  7018  genpelvu  7019  genpcdl  7025  genpcuu  7026  genprndl  7027  genprndu  7028  genpdisj  7029  addnqprllem  7033  addnqprulem  7034  addlocprlemeq  7039  addlocprlemgt  7040  nqprloc  7051  nqprl  7057  nqpru  7058  addnqprlemrl  7063  addnqprlemru  7064  addnqprlemfl  7065  addnqprlemfu  7066  prmuloc  7072  prmuloc2  7073  mullocpr  7077  mulnqprlemrl  7079  mulnqprlemru  7080  mulnqprlemfl  7081  mulnqprlemfu  7082  distrlem4prl  7090  distrlem4pru  7091  ltprordil  7095  1idprl  7096  1idpru  7097  ltpopr  7101  ltsopr  7102  ltaddpr  7103  ltexprlemm  7106  ltexprlemlol  7108  ltexprlemupu  7110  ltexprlemdisj  7112  ltexprlemloc  7113  ltexprlemrl  7116  ltexprlemru  7118  addcanprleml  7120  addcanprlemu  7121  addcanprg  7122  ltaprg  7125  recexprlemlol  7132  recexprlemdisj  7136  recexprlemloc  7137  recexprlem1ssl  7139  recexprlem1ssu  7140  aptiprleml  7145  aptiprlemu  7146  ltmprr  7148  archpr  7149  cauappcvgprlemm  7151  cauappcvgprlemopl  7152  cauappcvgprlemlol  7153  cauappcvgprlemopu  7154  cauappcvgprlemrnd  7156  cauappcvgprlemloc  7158  cauappcvgprlemladdfu  7160  cauappcvgprlemladdfl  7161  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  caucvgprlemnkj  7172  caucvgprlemm  7174  caucvgprlemopl  7175  caucvgprlemlol  7176  caucvgprlemopu  7177  caucvgprlemrnd  7179  caucvgprlemloc  7181  caucvgprlemladdfu  7183  caucvgprlemladdrl  7184  caucvgprlemlim  7187  caucvgprprlemnkltj  7195  caucvgprprlemnkeqj  7196  caucvgprprlemnjltk  7197  caucvgprprlemml  7200  caucvgprprlemopl  7203  caucvgprprlemlol  7204  caucvgprprlemopu  7205  caucvgprprlemrnd  7207  caucvgprprlemloc  7209  caucvgprprlemexbt  7212  caucvgprprlemexb  7213  caucvgprprlemlim  7217  mulcmpblnrlemg  7233  addsrmo  7236  mulsrmo  7237  ltsrprg  7240  srpospr  7275  caucvgsrlemgt1  7287  pitonn  7332  nntopi  7376  axcaucvglemcau  7380  axcaucvglemres  7381  lelttr  7520  ltletr  7521  readdcan  7569  cnegexlem1  7604  cnegexlem2  7605  addid0  7798  lelttrdi  7851  add20  7899  recexre  7999  inelr  8005  rimul  8006  apreap  8008  ltmul1  8013  cru  8023  apreim  8024  apirr  8026  apsym  8027  apcotr  8028  apadd1  8029  apneg  8032  mulext1  8033  msqge0  8037  mulge0  8040  apti  8043  ltleap  8051  recexap  8064  mulap0b  8066  recgt0  8249  prodgt02  8252  prodge02  8254  lemul12b  8260  lemul12a  8261  nnrecgt0  8397  addltmul  8588  nominpos  8589  elnnz  8696  peano2z  8722  zaddcllempos  8723  zaddcl  8726  zletric  8730  zlelttric  8731  zltnle  8732  zleloe  8733  zrevaddcl  8736  nzadd  8738  zdceq  8758  zdcle  8759  zdclt  8760  nn0n0n1ge2b  8762  nn0lt2  8764  zextle  8773  peano5uzti  8790  uzind2  8794  fzind  8797  fnn0ind  8798  nn0ind-raph  8799  btwnz  8801  eluzuzle  8962  uz11  8976  eluzp1m1  8977  supinfneg  9018  infsupneg  9019  lbzbi  9036  qapne  9059  qreccl  9062  qrevaddcl  9064  irradd  9066  irrmul  9067  ledivge1le  9138  nn0ledivnn  9173  xrlelttr  9206  xrltletr  9207  ixxss1  9257  ixxss2  9258  ixxss12  9259  iccid  9278  elioc2  9289  elico2  9290  elicc2  9291  fznlem  9390  fzn  9391  fzen  9392  0fz1  9394  uzsubsubfz  9396  fzopth  9409  fzss1  9411  fzss2  9412  elfz1b  9437  uzsplit  9439  fzm1  9447  fznuz  9449  fzrevral  9452  elfz0ubfz0  9467  elfz0fzfz0  9468  fz0fzelfz0  9469  difelfzle  9476  1fv  9481  fzoss1  9513  fzosplit  9519  fzouzsplit  9521  fzonmapblen  9529  fzofzim  9530  eluzgtdifelfzo  9539  elfzodifsumelfzo  9543  elfzom1p1elfzo  9556  ssfzo12  9566  ssfzo12bi  9567  fzofzp1b  9570  elfzonelfzo  9572  subfzo0  9584  qtri3or  9585  qletric  9586  qlelttric  9587  qltnle  9588  qdceq  9589  exbtwnzlemstep  9590  exbtwnzlemshrink  9591  exbtwnzlemex  9592  exbtwnz  9593  rebtwn2zlemstep  9595  rebtwn2z  9597  ioom  9603  ico0  9604  ioc0  9605  flltdivnn0lt  9642  flqeqceilz  9656  modqid2  9689  modqmuladd  9704  modqmuladdim  9705  modqmuladdnn0  9706  modqm1p1mod0  9713  modaddmodlo  9726  modfzo0difsn  9733  addmodlteq  9736  frec2uzuzd  9740  frec2uzltd  9741  frec2uzlt2d  9742  frec2uzrand  9743  frec2uzf1od  9744  frec2uzrdg  9747  frecuzrdgtcl  9750  frecuzrdgdomlem  9755  frecuzrdgfunlem  9757  frecfzennn  9764  uzsinds  9779  iseqclt  9801  iseqoveq  9802  iseqf1olemqf1o  9830  iseqf1olemp  9839  iseqid3s  9845  iseqid  9846  iseqz  9849  expival  9859  expcl2lemap  9869  leexp2r  9911  leexp1a  9912  zesq  9972  expnbnd  9977  nn0opthlem2d  10029  nn0opthd  10030  facdiv  10046  facndiv  10047  facwordi  10048  faclbnd  10049  faclbnd6  10052  facubnd  10053  bcval4  10060  bcpasc  10074  bccl  10075  fiinfnf1o  10094  fihashf1rn  10097  hashunlem  10112  fiprsshashgt1  10125  hashfzo  10130  hashfzp1  10132  hashxp  10134  hashfacen  10141  zfz1iso  10146  iseqcoll  10147  ovshftex  10153  reim0b  10195  cjap  10239  caucvgrelemcau  10312  caucvgre  10313  cvg1nlemres  10317  r19.29uz  10324  r19.2uz  10325  recvguniq  10327  sqrt0  10336  resqrexlemover  10342  resqrexlemdecn  10344  resqrexlemlo  10345  resqrexlemcalc3  10348  resqrexlemglsq  10354  resqrexlemga  10355  rsqrmo  10359  sqrtsq  10376  abs00ap  10394  absnid  10405  qabsor  10407  absexpzap  10412  abs3lem  10443  cau3lem  10446  caubnd2  10449  icodiamlt  10512  maxleim  10537  maxabslemlub  10539  maxabslemval  10540  fimaxre2  10556  negfi  10557  minmax  10559  clim  10567  climuni  10579  climcn1  10594  climcn2  10595  mulcn2  10598  iiserex  10624  climcau  10631  climcaucn  10635  isumrblem  10660  fisumcvg  10661  isummolem2a  10665  zisum  10668  fisum  10670  isumz  10672  fsumf1o  10673  fisumss  10675  fisumcvg3  10679  fsumsplit  10689  dvdsval2  10705  moddvds  10711  dvds0  10717  absdvdsb  10720  dvdsabsb  10721  dvdsmul1  10724  dvdscmul  10729  dvdsmulc  10730  dvds2ln  10735  dvds2add  10736  dvds2sub  10737  dvdslelemd  10750  dvdsleabs2  10753  dvds1  10760  dvdsext  10762  fzo0dvdseq  10764  dvdsfac  10767  mulmoddvds  10770  odd2np1  10779  oddge22np1  10787  evennn02n  10788  evennn2n  10789  mulsucdiv2z  10791  sqoddm1div8z  10792  ltoddhalfle  10799  halfleoddlt  10800  m1expo  10806  nn0ehalf  10809  nn0o  10813  nn0oddm1d2  10815  nnoddm1d2  10816  divalglemeunn  10827  divalglemex  10828  divalglemeuneg  10829  flodddiv4  10840  zsupcllemstep  10847  dvdsbnd  10854  dvdslegcd  10862  gcdeq0  10874  gcd0id  10876  gcdneg  10879  gcdaddm  10881  gcdabs  10885  bezoutlemnewy  10891  bezoutlemstep  10892  bezoutlemzz  10897  bezoutlemaz  10898  bezoutlembz  10899  bezoutlembi  10900  bezoutlemeu  10902  bezoutlemle  10903  bezoutlemsup  10904  dvdsgcd  10907  dfgcd2  10909  rppwr  10923  dvdssqlem  10925  bezoutr1  10928  ialgfx  10940  eucalglt  10945  eucialgcvga  10946  lcmledvds  10958  lcmeq0  10959  lcmneg  10962  lcmabs  10964  lcmgcdlem  10965  lcmdvds  10967  lcmgcdeq  10971  coprmgcdb  10976  ncoprmgcdne1b  10977  coprmdvds  10980  qredeq  10984  qredeu  10985  rpdvds  10987  divgcdcoprm0  10989  divgcdcoprmex  10990  cncongr1  10991  cncongr2  10992  isprm2lem  11004  prmind2  11008  dvdsnprmd  11013  divgcdodd  11028  coprm  11029  isprm6  11032  prmfac1  11037  rpexp  11038  sqrt2irr  11047  pw2dvdseu  11052  sqrt2irrap  11064  nonsq  11091  hashdvds  11103  phimullem  11107  cbvrald  11157  uzdcinzz  11167  bdsepnft  11247  peano5set  11304  findset  11309  bj-omtrans  11320  bj-findis  11343  strcollnft  11348  nnpredcl  11359  peano4nninf  11365  nninfalllem1  11368  nninfall  11369  nninfsellemqall  11376  nninfomnilem  11379  exmidsbthrlem  11381  exmidsbth  11383
  Copyright terms: Public domain W3C validator