ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ex Structured version   GIF 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 ((φ ψ) → χ)
Assertion
Ref Expression
ex (φ → (ψχ))

Proof of Theorem ex
StepHypRef Expression
1 ax-ia3 101 . 2 (φ → (ψ → (φ ψ)))
2 exp.1 . 2 ((φ ψ) → χ)
31, 2syl6 29 1 (φ → (ψχ))
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  pm3.2  126  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  564  pm2.65da  586  mtand  590  pm5.21im  611  jao  671  jaoian  708  jaodan  709  impidc  754  pm2.5dc  762  con1bidc  767  con2bidc  768  con1bdc  771  pm5.18dc  776  dfandc  777  pm4.63dc  779  dcim  783  pm4.54dc  804  pm5.21nd  824  dcan  841  dcor  842  annimdc  844  pm4.55dc  845  pm3.11dc  863  pm3.12dc  864  prlem1  879  pm3.2an3  1082  3jcad  1084  3impia  1100  3an1rs  1115  3exp1  1119  3exp2  1121  exp520  1124  syl3anl2  1183  3jaoian  1199  3jaodan  1200  mp3anl1  1225  mp3anl2  1226  mp3anl3  1227  inegd  1262  xor3dc  1275  pm5.15dc  1277  xor2dc  1278  xornbidc  1279  xordc  1280  nbbndc  1282  biassdc  1283  dfbi3dc  1285  pm5.24dc  1286  alanimi  1345  equsexd  1614  sbequ1  1648  sbiedv  1669  ax11v2  1698  equs5or  1708  sbequi  1717  exlimdd  1749  exlimddv  1775  cbvaldva  1800  cbvexdva  1801  nfsbxyt  1816  sbcomxyyz  1843  nfsb4t  1887  eupickbi  1979  moexexdc  1981  euexex  1982  2euswapdc  1988  dvelimdc  2194  nebidc  2279  rgen2a  2369  ralimiaa  2377  ralimdaa  2380  ralrimiva  2386  ralrimdva  2393  ralrimivva  2395  ralrimdvv  2397  ralrimdvva  2398  reximdva  2415  rexlimiva  2422  rexlimdva  2427  rexlimdvva  2434  r19.29vva  2450  2gencl  2581  vtocldf  2599  spcimdv  2631  spcimedv  2633  rspct  2643  eqvinc  2661  eqvincg  2662  ceqex  2665  reu6  2724  eqreu  2727  sbciedf  2792  rmob  2844  csbiebt  2880  csbiedf  2881  reupick  3215  reximdva0m  3230  ssn0  3253  rgenm  3317  preqr1g  3528  prel12  3533  dfnfc2  3589  intssunim  3628  intab  3635  iineq2d  3668  ssiun2  3691  mpteq2da  3837  trintssm  3861  copsexg  3972  copsex2t  3973  sess1  4059  sess2  4060  tron  4085  onelss  4090  onintss  4093  reusv1  4156  reusv3  4158  rabxfrd  4167  iunpw  4177  ssorduni  4179  ordsson  4184  ordsucg  4194  onsucelsucexmidlem  4214  elirr  4224  en2lp  4232  ordsuc  4241  ordpwsucss  4243  tfisi  4253  sosng  4356  2optocl  4360  relop  4429  xpid11m  4500  releldmb  4514  relelrnb  4515  elrnmptg  4529  elreimasng  4634  relbrcnvg  4647  trin2  4659  ssxpbm  4699  ssxp1  4700  ssxp2  4701  elxp4  4751  elxp5  4752  relresfld  4790  relcoi1  4792  iotaval  4821  iotass  4827  funmo  4860  imadif  4922  imain  4924  2elresin  4953  feu  5015  fcnvres  5016  f1oun  5089  f1oprg  5111  relfvssunirn  5134  funbrfv  5155  funbrfv2b  5161  dffn5im  5162  dfimafn  5165  funimass4  5167  ssimaex  5177  fvmptssdm  5198  fvmptf  5206  fvimacnv  5225  funimass3  5226  elpreima  5229  elrnrexdm  5249  eldmrexrn  5251  dffo4  5258  dffo5  5259  fmpt  5262  ffvresb  5271  fmptco  5273  fsn  5278  funfvima  5333  funfvima2  5334  f1mpt  5353  f1imass  5356  f1ocnvfvrneq  5365  foeqcnvco  5373  f1eqcocnv  5374  fliftfun  5379  fliftf  5382  isopolem  5404  isosolem  5406  eusvobj2  5441  acexmidlemab  5449  oprabid  5480  ovidi  5561  ovg  5581  suppssfv  5650  suppssov1  5651  funrnex  5683  f1dmex  5685  oprabexd  5696  fo2ndresm  5731  op1steq  5747  dfoprab3  5759  fo2ndf  5790  f1o2ndf1  5791  poxp  5794  isprmpt2  5799  reldmtpos  5809  rntpos  5813  tposf2  5824  tposf12  5825  issmo2  5845  smores  5848  smoiso  5858  tfrlem9  5876  tfrlemibacc  5881  tfrlemibfn  5883  tfrlemi14d  5888  tfrexlem  5889  rdgivallem  5908  frecsuclem3  5929  frecrdg  5931  freccl  5932  oawordi  5988  nnmcom  6007  nnsucelsuc  6009  nntri3or  6011  nntri1  6013  nnaordi  6017  nnmord  6026  nnaordex  6036  nnm00  6038  ertr  6057  erex  6066  iserd  6068  iinerm  6114  erinxp  6116  qsel  6119  qliftfun  6124  qliftfund  6125  2ecoptocl  6130  brecop  6132  dom2lem  6188  fundmen  6222  unen  6229  enm  6230  xpdom2  6241  fopwdom  6246  mulcanpig  6319  nlt1pig  6325  addcmpblnq  6351  ltsonq  6382  ltexnqq  6391  prarloclemarch2  6402  enq0tr  6417  addcmpblnq0  6426  addnq0mo  6430  mulnq0mo  6431  prcdnql  6467  prcunqu  6468  prarloclemlo  6477  prarloclem3step  6479  prarloclem3  6480  genpdflem  6490  genpelvl  6495  genpelvu  6496  genpcdl  6502  genpcuu  6503  genprndl  6504  genprndu  6505  genpdisj  6506  addnqprllem  6510  addnqprulem  6511  addlocprlemeq  6516  addlocprlemgt  6517  nqprloc  6528  nqprl  6533  addnqprlemrl  6538  addnqprlemru  6539  addnqprlemfl  6540  addnqprlemfu  6541  prmuloc  6547  prmuloc2  6548  mullocpr  6552  distrlem4prl  6560  distrlem4pru  6561  ltprordil  6565  1idprl  6566  1idpru  6567  ltpopr  6569  ltsopr  6570  ltaddpr  6571  ltexprlemm  6574  ltexprlemlol  6576  ltexprlemupu  6578  ltexprlemdisj  6580  ltexprlemloc  6581  ltexprlemrl  6584  ltexprlemru  6586  addcanprleml  6588  addcanprlemu  6589  addcanprg  6590  ltaprg  6592  recexprlemlol  6598  recexprlemdisj  6602  recexprlemloc  6603  recexprlem1ssl  6605  recexprlem1ssu  6606  aptiprleml  6611  aptiprlemu  6612  ltmprr  6614  archpr  6615  cauappcvgprlemm  6617  cauappcvgprlemopl  6618  cauappcvgprlemlol  6619  cauappcvgprlemopu  6620  cauappcvgprlemrnd  6622  cauappcvgprlemloc  6624  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  caucvgprlemnkj  6637  caucvgprlemm  6639  caucvgprlemopl  6640  caucvgprlemlol  6641  caucvgprlemopu  6642  caucvgprlemrnd  6644  caucvgprlemloc  6646  caucvgprlemladdfu  6648  caucvgprlemladdrl  6649  caucvgprlemlim  6652  mulcmpblnrlemg  6668  addsrmo  6671  mulsrmo  6672  ltsrprg  6675  pitonn  6744  lelttr  6903  ltletr  6904  readdcan  6950  cnegexlem1  6983  cnegexlem2  6984  add20  7264  recexre  7362  inelr  7368  rimul  7369  apreap  7371  ltmul1  7376  cru  7386  apreim  7387  apirr  7389  apsym  7390  apcotr  7391  apadd1  7392  apneg  7395  mulext1  7396  msqge0  7400  mulge0  7403  apti  7406  ltleap  7413  recexap  7416  mulap0b  7418  recgt0  7597  prodgt02  7600  prodge02  7602  lemul12b  7608  lemul12a  7609  nnrecgt0  7732  addltmul  7938  nominpos  7939  elnnz  8031  peano2z  8057  zaddcllempos  8058  zaddcl  8061  zletric  8065  zlelttric  8066  zltnle  8067  zleloe  8068  zrevaddcl  8071  zdceq  8092  zdcle  8093  zdclt  8094  nn0n0n1ge2b  8096  nn0lt2  8098  zextle  8107  peano5uzti  8122  uzind2  8126  fzind  8129  fnn0ind  8130  nn0ind-raph  8131  btwnz  8133  eluzuzle  8257  uz11  8271  eluzp1m1  8272  lbzbi  8327  qapne  8350  qreccl  8351  qrevaddcl  8353  irradd  8355  irrmul  8356  xrlelttr  8492  xrltletr  8493  ixxss1  8543  ixxss2  8544  ixxss12  8545  iccid  8564  elioc2  8575  elico2  8576  elicc2  8577  fznlem  8675  fzn  8676  fzen  8677  0fz1  8679  uzsubsubfz  8681  fzopth  8694  fzss1  8696  fzss2  8697  elfz1b  8722  uzsplit  8724  fzm1  8732  fznuz  8734  fzrevral  8737  elfz0ubfz0  8752  elfz0fzfz0  8753  fz0fzelfz0  8754  difelfzle  8762  1fv  8766  fzoss1  8797  fzosplit  8803  fzouzsplit  8805  fzonmapblen  8813  fzofzim  8814  eluzgtdifelfzo  8823  elfzodifsumelfzo  8827  elfzom1p1elfzo  8840  ssfzo12  8850  ssfzo12bi  8851  fzofzp1b  8854  elfzonelfzo  8856  frec2uzzd  8867  frec2uzuzd  8869  frec2uzltd  8870  frec2uzlt2d  8871  frec2uzrand  8872  frec2uzf1od  8873  frec2uzrdg  8876  frecuzrdgfn  8879  frecfzennn  8884  expival  8911  expcl2lemap  8921  leexp2r  8962  leexp1a  8963  zesq  9020  expnbnd  9025  reim0b  9090  cjap  9134  sqrt0  9213  sqrtsq  9214  absnid  9227  cbvrald  9262  bdsepnft  9342  peano5set  9399  peano5setOLD  9400  findset  9405  bj-omtrans  9416  bj-findis  9439  strcollnft  9444
  Copyright terms: Public domain W3C validator