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

Theorem ex 112
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 105 . 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 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  expcom  113  bi3  116  expd  249  impancom  251  expimpd  349  exp31  350  exp32  351  exp4b  353  exp41  356  exp43  358  exp53  363  impr  365  simplbi2  371  anidms  383  syl2anc  397  pm5.74da  425  imdistanda  430  pm5.32da  433  impbida  538  anim12dan  542  pm2.01da  575  pm2.65da  597  mtand  601  pm5.21im  622  jao  682  jaoian  719  jaodan  721  impidc  766  pm2.5dc  774  con1bidc  779  con2bidc  780  con1bdc  783  pm5.18dc  788  dfandc  789  pm4.63dc  791  dcim  795  pm4.54dc  816  pm5.21nd  836  dcan  853  dcor  854  annimdc  856  pm4.55dc  857  pm3.11dc  875  pm3.12dc  876  prlem1  891  pm3.2an3  1094  3jcad  1096  3impia  1112  3an1rs  1127  3exp1  1131  3exp2  1133  exp520  1136  syl3anl2  1195  3jaoian  1211  3jaodan  1212  mp3anl1  1237  mp3anl2  1238  mp3anl3  1239  inegd  1279  xor3dc  1294  pm5.15dc  1296  xor2dc  1297  xornbidc  1298  xordc  1299  nbbndc  1301  biassdc  1302  dfbi3dc  1304  pm5.24dc  1305  alanimi  1364  equsexd  1633  sbequ1  1667  sbiedv  1688  ax11v2  1717  equs5or  1727  sbequi  1736  exlimdd  1768  exlimddv  1794  cbvaldva  1819  cbvexdva  1820  nfsbxyt  1835  sbcomxyyz  1862  nfsb4t  1906  eupickbi  1998  moexexdc  2000  euexex  2001  2euswapdc  2007  dvelimdc  2213  nebidc  2300  rgen2a  2392  ralimiaa  2400  ralimdaa  2403  ralrimiva  2409  ralrimdva  2416  ralrimivva  2418  ralrimdvv  2420  ralrimdvva  2421  reximdva  2438  rexlimiva  2445  rexlimdva  2450  rexlimdvva  2457  r19.29vva  2473  2gencl  2604  vtocldf  2622  spcimdv  2654  spcimedv  2656  rspct  2666  eqvinc  2689  eqvincg  2690  ceqex  2693  reu6  2752  eqreu  2755  sbciedf  2820  rmob  2877  csbiebt  2913  csbiedf  2914  reupick  3248  reximdva0m  3263  ssn0  3286  rgenm  3350  preqr1g  3564  prel12  3569  dfnfc2  3625  intssunim  3664  intab  3671  iineq2d  3704  ssiun2  3727  mpteq2da  3873  trintssmOLD  3898  copsexg  4008  copsex2t  4009  sess1  4101  sess2  4102  frirrg  4114  tron  4146  onelss  4151  onintss  4154  reusv1  4217  reusv3  4219  rabxfrd  4228  iunpw  4238  ssorduni  4240  ordsson  4245  ordsucg  4255  onintrab2im  4271  onsucelsucexmidlem  4281  elirr  4293  en2lp  4305  ordsuc  4314  ordpwsucss  4318  ordtri2or2exmid  4323  reg3exmidlemwe  4330  tfisi  4337  sosng  4440  2optocl  4444  relop  4513  xpid11m  4584  releldmb  4598  relelrnb  4599  elrnmptg  4613  elreimasng  4718  relbrcnvg  4731  trin2  4743  ssxpbm  4783  ssxp1  4784  ssxp2  4785  elxp4  4835  elxp5  4836  relresfld  4874  relcoi1  4876  iotaval  4905  iotass  4911  funmo  4944  imadif  5006  imain  5008  2elresin  5037  feu  5099  fcnvres  5100  f1oun  5173  f1oprg  5195  relfvssunirn  5218  funbrfv  5239  funbrfv2b  5245  dffn5im  5246  dfimafn  5249  funimass4  5251  ssimaex  5261  fvmptssdm  5282  fvmptf  5290  fvimacnv  5309  funimass3  5310  elpreima  5313  elrnrexdm  5333  eldmrexrn  5335  dffo4  5342  dffo5  5343  fmpt  5346  ffvresb  5355  fmptco  5357  fsn  5362  funfvima  5417  funfvima2  5418  f1mpt  5437  f1imass  5440  f1ocnvfvrneq  5449  foeqcnvco  5457  f1eqcocnv  5458  fliftfun  5463  fliftf  5466  isopolem  5488  isosolem  5490  eusvobj2  5525  acexmidlemab  5533  oprabid  5564  ovidi  5646  ovg  5666  suppssfv  5735  suppssov1  5736  funrnex  5768  f1dmex  5770  oprabexd  5781  fo2ndresm  5816  op1steq  5832  dfoprab3  5844  fo2ndf  5875  f1o2ndf1  5876  poxp  5880  spc2ed  5881  f1od2  5883  isprmpt2  5888  reldmtpos  5898  rntpos  5902  tposf2  5913  tposf12  5914  issmo2  5934  smores  5937  smoiso  5947  tfrlem9  5965  tfrlemibacc  5970  tfrlemibfn  5972  tfrlemi14d  5977  tfrexlem  5978  rdgivallem  5998  frecsuclem3  6020  frecrdg  6022  freccl  6023  oawordi  6079  nnmcom  6098  nnsucelsuc  6100  nntri3or  6102  nntri1  6104  nnsseleq  6109  nndifsnid  6110  nnaordi  6111  nnmord  6120  nnaordex  6130  nnm00  6132  ertr  6151  erex  6160  iserd  6162  iinerm  6208  erinxp  6210  qsel  6213  qliftfun  6218  qliftfund  6219  2ecoptocl  6224  brecop  6226  dom2lem  6282  fundmen  6316  unen  6323  enm  6324  xpdom2  6335  fopwdom  6340  phplem4  6348  nneneq  6350  snnen2og  6352  phplem4dom  6354  nndomo  6356  phpm  6357  phplem4on  6359  fidifsnen  6361  fidifsnid  6362  fin0  6372  fin0or  6373  findcard2  6376  findcard2s  6377  findcard2d  6378  findcard2sd  6379  ac6sfi  6382  onunsnss  6385  eqsupti  6401  isotilem  6409  supisoex  6412  ordiso2  6414  mulcanpig  6490  nlt1pig  6496  addcmpblnq  6522  ltsonq  6553  ltexnqq  6563  prarloclemarch2  6574  enq0tr  6589  addcmpblnq0  6598  addnq0mo  6602  mulnq0mo  6603  prcdnql  6639  prcunqu  6640  prarloclemlo  6649  prarloclem3step  6651  prarloclem3  6652  genpdflem  6662  genpelvl  6667  genpelvu  6668  genpcdl  6674  genpcuu  6675  genprndl  6676  genprndu  6677  genpdisj  6678  addnqprllem  6682  addnqprulem  6683  addlocprlemeq  6688  addlocprlemgt  6689  nqprloc  6700  nqprl  6706  nqpru  6707  addnqprlemrl  6712  addnqprlemru  6713  addnqprlemfl  6714  addnqprlemfu  6715  prmuloc  6721  prmuloc2  6722  mullocpr  6726  mulnqprlemrl  6728  mulnqprlemru  6729  mulnqprlemfl  6730  mulnqprlemfu  6731  distrlem4prl  6739  distrlem4pru  6740  ltprordil  6744  1idprl  6745  1idpru  6746  ltpopr  6750  ltsopr  6751  ltaddpr  6752  ltexprlemm  6755  ltexprlemlol  6757  ltexprlemupu  6759  ltexprlemdisj  6761  ltexprlemloc  6762  ltexprlemrl  6765  ltexprlemru  6767  addcanprleml  6769  addcanprlemu  6770  addcanprg  6771  ltaprg  6774  recexprlemlol  6781  recexprlemdisj  6785  recexprlemloc  6786  recexprlem1ssl  6788  recexprlem1ssu  6789  aptiprleml  6794  aptiprlemu  6795  ltmprr  6797  archpr  6798  cauappcvgprlemm  6800  cauappcvgprlemopl  6801  cauappcvgprlemlol  6802  cauappcvgprlemopu  6803  cauappcvgprlemrnd  6805  cauappcvgprlemloc  6807  cauappcvgprlemladdfu  6809  cauappcvgprlemladdfl  6810  cauappcvgprlemladdru  6811  cauappcvgprlemladdrl  6812  caucvgprlemnkj  6821  caucvgprlemm  6823  caucvgprlemopl  6824  caucvgprlemlol  6825  caucvgprlemopu  6826  caucvgprlemrnd  6828  caucvgprlemloc  6830  caucvgprlemladdfu  6832  caucvgprlemladdrl  6833  caucvgprlemlim  6836  caucvgprprlemnkltj  6844  caucvgprprlemnkeqj  6845  caucvgprprlemnjltk  6846  caucvgprprlemml  6849  caucvgprprlemopl  6852  caucvgprprlemlol  6853  caucvgprprlemopu  6854  caucvgprprlemrnd  6856  caucvgprprlemloc  6858  caucvgprprlemexbt  6861  caucvgprprlemexb  6862  caucvgprprlemlim  6866  mulcmpblnrlemg  6882  addsrmo  6885  mulsrmo  6886  ltsrprg  6889  srpospr  6924  caucvgsrlemgt1  6936  pitonn  6981  nntopi  7025  axcaucvglemcau  7029  axcaucvglemres  7030  lelttr  7164  ltletr  7165  readdcan  7213  cnegexlem1  7248  cnegexlem2  7249  addid0  7442  lelttrdi  7494  add20  7542  recexre  7642  inelr  7648  rimul  7649  apreap  7651  ltmul1  7656  cru  7666  apreim  7667  apirr  7669  apsym  7670  apcotr  7671  apadd1  7672  apneg  7675  mulext1  7676  msqge0  7680  mulge0  7683  apti  7686  ltleap  7694  recexap  7707  mulap0b  7709  recgt0  7890  prodgt02  7893  prodge02  7895  lemul12b  7901  lemul12a  7902  nnrecgt0  8026  addltmul  8217  nominpos  8218  elnnz  8311  peano2z  8337  zaddcllempos  8338  zaddcl  8341  zletric  8345  zlelttric  8346  zltnle  8347  zleloe  8348  zrevaddcl  8351  nzadd  8353  zdceq  8373  zdcle  8374  zdclt  8375  nn0n0n1ge2b  8377  nn0lt2  8379  zextle  8388  peano5uzti  8404  uzind2  8408  fzind  8411  fnn0ind  8412  nn0ind-raph  8413  btwnz  8415  eluzuzle  8576  uz11  8590  eluzp1m1  8591  lbzbi  8647  qapne  8670  qreccl  8673  qrevaddcl  8675  irradd  8677  irrmul  8678  ledivge1le  8749  nn0ledivnn  8784  xrlelttr  8822  xrltletr  8823  ixxss1  8873  ixxss2  8874  ixxss12  8875  iccid  8894  elioc2  8905  elico2  8906  elicc2  8907  fznlem  9006  fzn  9007  fzen  9008  0fz1  9010  uzsubsubfz  9012  fzopth  9025  fzss1  9027  fzss2  9028  elfz1b  9053  uzsplit  9055  fzm1  9063  fznuz  9065  fzrevral  9068  elfz0ubfz0  9083  elfz0fzfz0  9084  fz0fzelfz0  9085  difelfzle  9093  1fv  9097  fzoss1  9128  fzosplit  9134  fzouzsplit  9136  fzonmapblen  9144  fzofzim  9145  eluzgtdifelfzo  9154  elfzodifsumelfzo  9158  elfzom1p1elfzo  9171  ssfzo12  9181  ssfzo12bi  9182  fzofzp1b  9185  elfzonelfzo  9187  subfzo0  9198  qtri3or  9199  qletric  9200  qlelttric  9201  qltnle  9202  qdceq  9203  qbtwnzlemstep  9204  qbtwnzlemex  9206  qbtwnz  9207  rebtwn2zlemstep  9208  rebtwn2z  9210  flltdivnn0lt  9248  flqeqceilz  9262  modqid2  9295  modqmuladd  9310  modqmuladdim  9311  modqmuladdnn0  9312  modqm1p1mod0  9319  modaddmodlo  9332  modfzo0difsn  9339  addmodlteq  9342  frec2uzzd  9344  frec2uzuzd  9346  frec2uzltd  9347  frec2uzlt2d  9348  frec2uzrand  9349  frec2uzf1od  9350  frec2uzrdg  9353  frecuzrdgfn  9356  frecfzennn  9361  iseqid3s  9404  iseqid  9405  iseqz  9407  expival  9416  expcl2lemap  9426  leexp2r  9468  leexp1a  9469  zesq  9528  expnbnd  9533  nn0opthlem2d  9582  nn0opthd  9583  facdiv  9599  facndiv  9600  facwordi  9601  faclbnd  9602  faclbnd6  9605  facubnd  9606  bcval4  9613  bcpasc  9627  bccl  9628  ovshftex  9641  reim0b  9683  cjap  9727  caucvgrelemcau  9800  caucvgre  9801  cvg1nlemres  9805  r19.29uz  9811  r19.2uz  9812  recvguniq  9814  sqrt0  9823  resqrexlemover  9829  resqrexlemdecn  9831  resqrexlemlo  9832  resqrexlemcalc3  9835  resqrexlemglsq  9841  resqrexlemga  9842  rsqrmo  9846  sqrtsq  9863  abs00ap  9881  absnid  9892  qabsor  9894  absexpzap  9899  abs3lem  9930  cau3lem  9933  caubnd2  9936  icodiamlt  9999  clim  10025  climuni  10037  climcn1  10052  climcn2  10053  mulcn2  10056  iiserex  10082  climcau  10089  climcaucn  10093  dvdsval2  10103  moddvds  10109  dvds0  10115  absdvdsb  10118  dvdsabsb  10119  dvdsmul1  10121  dvdscmul  10126  dvdsmulc  10127  dvds2ln  10132  dvds2add  10133  dvds2sub  10134  dvdslelemd  10147  dvdsleabs2  10150  dvds1  10157  dvdsext  10159  fzo0dvdseq  10161  dvdsfac  10164  mulmoddvds  10167  odd2np1  10176  oddge22np1  10185  evennn02n  10186  evennn2n  10187  mulsucdiv2z  10189  sqoddm1div8z  10190  ltoddhalfle  10197  halfleoddlt  10198  m1expo  10204  nn0ehalf  10207  nn0o  10211  nn0oddm1d2  10213  nnoddm1d2  10214  sqrt2irr  10223  pw2dvdseu  10228  ialgfx  10246  cbvrald  10286  bdsepnft  10366  peano5set  10423  peano5setOLD  10424  findset  10429  bj-omtrans  10440  bj-findis  10463  strcollnft  10468
  Copyright terms: Public domain W3C validator