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  379  syl2anc  393  pm5.74da  420  imdistanda  425  pm5.32da  428  impbida  515  anim12dan  519  pm2.01da  552  pm2.65da  574  mtand  578  pm5.21im  599  jao  659  jaoian  696  jaodan  697  impidc  743  pm2.5dc  751  con1bidc  756  con2bidc  757  con1bdc  760  pm5.18dc  765  dfandc  766  pm4.63dc  768  dcim  772  pm4.54dc  793  pm5.21nd  813  dcan  828  dcor  829  annimdc  831  pm4.55dc  832  pm3.11dc  850  pm3.12dc  851  prlem1  866  pm3.2an3  1066  3jcad  1068  3impia  1085  3an1rs  1100  3exp1  1104  3exp2  1106  exp520  1109  syl3anl2  1168  3jaoian  1184  3jaodan  1185  mp3anl1  1209  mp3anl2  1210  mp3anl3  1211  inegd  1246  xor3dc  1259  pm5.15dc  1261  xor2dc  1262  xornbidc  1263  xordc  1264  nbbndc  1266  biassdc  1267  dfbi3dc  1269  pm5.24dc  1270  alanimi  1324  equsexd  1595  sbequ1  1629  sbiedv  1650  ax11v2  1679  equs5or  1689  sbequi  1698  exlimdd  1730  exlimddv  1756  cbvaldva  1781  cbvexdva  1782  nfsbxyt  1797  sbcomxyyz  1824  nfsb4t  1868  eupickbi  1960  moexexdc  1962  euexex  1963  2euswapdc  1969  dvelimdc  2175  nebidc  2259  rgen2a  2349  ralimiaa  2357  ralimdaa  2360  ralrimiva  2366  ralrimdva  2373  ralrimivva  2375  ralrimdvv  2377  ralrimdvva  2378  reximdva  2395  rexlimiva  2402  rexlimdva  2407  rexlimdvva  2414  r19.29_2a  2430  2gencl  2560  vtocldf  2578  spcimdv  2610  spcimedv  2612  rspct  2622  eqvinc  2640  eqvincg  2641  ceqex  2644  reu6  2703  eqreu  2706  sbciedf  2771  rmob  2823  csbiebt  2859  csbiedf  2860  reupick  3194  reximdva0m  3209  ssn0  3232  rgenm  3298  preqr1g  3507  prel12  3512  dfnfc2  3568  intssunim  3607  intab  3614  iineq2d  3647  ssiun2  3670  mpteq2da  3816  trintssm  3840  copsexg  3951  copsex2t  3952  sess1  4038  sess2  4039  tron  4064  onelss  4069  onintss  4072  suctr  4104  reusv1  4136  reusv3  4138  rabxfrd  4147  iunpw  4157  ssorduni  4159  ordsson  4164  ordsucg  4174  onsucelsucexmidlem  4194  elirr  4204  en2lp  4212  ordsuc  4221  ordpwsucss  4223  tfisi  4233  sosng  4336  2optocl  4340  relop  4409  xpid11m  4480  releldmb  4494  relelrnb  4495  elrnmptg  4509  elreimasng  4614  relbrcnvg  4627  trin2  4639  ssxpbm  4679  ssxp1  4680  ssxp2  4681  elxp4  4731  elxp5  4732  relresfld  4770  relcoi1  4772  iotaval  4801  iotass  4807  funmo  4839  imadif  4901  imain  4903  2elresin  4932  feu  4993  fcnvres  4994  f1oun  5067  f1oprg  5089  relfvssunirn  5112  funbrfv  5133  funbrfv2b  5139  dffn5im  5140  dfimafn  5143  funimass4  5145  ssimaex  5155  fvmptssdm  5176  fvmptf  5184  fvimacnv  5203  funimass3  5204  elpreima  5207  elrnrexdm  5227  eldmrexrn  5229  dffo4  5236  dffo5  5237  fmpt  5240  ffvresb  5249  fmptco  5251  fsn  5256  funfvima  5311  funfvima2  5312  f1mpt  5331  f1imass  5334  f1ocnvfvrneq  5343  foeqcnvco  5351  f1eqcocnv  5352  fliftfun  5357  fliftf  5360  isopolem  5382  isosolem  5384  eusvobj2  5418  acexmidlemab  5426  oprabid  5457  ovidi  5538  ovg  5558  suppssfv  5627  suppssov1  5628  funrnex  5660  f1dmex  5662  oprabexd  5673  fo2ndresm  5708  op1steq  5724  dfoprab3  5736  fo2ndf  5767  f1o2ndf1  5768  poxp  5771  isprmpt2  5776  reldmtpos  5786  rntpos  5790  tposf2  5801  tposf12  5802  issmo2  5822  smores  5825  smoiso  5835  tfrlem9  5853  tfrlemibacc  5857  tfrlemibfn  5859  tfrlemi14d  5864  tfrexlem  5866  rdgi0g  5882  rdgivallem  5884  frecsuclem3  5902  frecrdg  5904  oawordi  5960  nnmcom  5979  nnsucelsuc  5981  nntri3or  5983  nntri1  5985  nnaordi  5988  nnmord  5997  nnaordex  6007  nnm00  6009  ertr  6028  erex  6037  iserd  6039  iinerm  6085  erinxp  6087  qsel  6090  qliftfun  6095  qliftfund  6096  2ecoptocl  6101  brecop  6103  mulcanpig  6189  nlt1pig  6195  addcmpblnq  6220  ltsonq  6251  ltexnqq  6260  prarloclemarch2  6270  enq0tr  6283  addcmpblnq0  6292  addnq0mo  6296  mulnq0mo  6297  prcdnql  6332  prcunqu  6333  prarloclemlo  6342  prarloclem3step  6344  prarloclem3  6345  genpdflem  6355  genpelvl  6360  genpelvu  6361  genpcdl  6368  genpcuu  6369  genprndl  6370  genprndu  6371  genpdisj  6372  addnqprllem  6376  addnqprulem  6377  addlocprlemeq  6382  addlocprlemgt  6383  nqprloc  6394  prmuloc  6404  prmuloc2  6405  mullocpr  6409  distrlem4prl  6417  distrlem4pru  6418  ltprordil  6422  1idprl  6423  1idpru  6424  ltpopr  6426  ltsopr  6427  ltaddpr  6428  ltexprlemm  6431  ltexprlemlol  6433  ltexprlemupu  6435  ltexprlemdisj  6437  ltexprlemloc  6438  ltexprlemrl  6441  ltexprlemru  6443  addcanprleml  6445  addcanprlemu  6446  addcanprg  6447  ltaprg  6449  recexprlemlol  6454  recexprlemdisj  6458  recexprlemloc  6459  recexprlem1ssl  6461  recexprlem1ssu  6462  mulcmpblnrlemg  6481  addsrmo  6484  mulsrmo  6485  ltsrprg  6488  lelttr  6698  ltletr  6699  readdcan  6740  cnegexlem1  6773  cnegexlem2  6774  cbvrald  7173  bdsepnft  7252  peano5set  7301  findset  7306  bj-omtrans  7317  bj-findis  7336  strcollnft  7341
  Copyright terms: Public domain W3C validator