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  513  anim12dan  517  pm2.01da  549  pm2.65da  571  mtand  575  pm5.21im  596  jao  656  jaoian  693  jaodan  694  impidc  739  pm2.5dc  747  con1bidc  752  con2bidc  753  con1bdc  756  pm5.18dc  761  dfandc  762  pm4.63dc  764  dcim  768  pm4.54dc  789  pm5.21nd  809  dcan  824  dcor  825  annimdc  827  pm4.55dc  828  pm3.11dc  846  pm3.12dc  847  prlem1  862  pm3.2an3  1065  3jcad  1067  3impia  1082  3an1rs  1097  3exp1  1101  3exp2  1103  exp520  1106  syl3anl2  1165  3jaoian  1181  3jaodan  1182  mp3anl1  1206  mp3anl2  1207  mp3anl3  1208  inegd  1243  xor3dc  1256  pm5.15dc  1258  xor2dc  1259  xornbidc  1260  xordc  1261  nbbndc  1263  biassdc  1264  dfbi3dc  1266  pm5.24dc  1267  alanimi  1321  equsexd  1590  sbequ1  1624  sbiedv  1645  ax11v2  1674  equs5or  1684  sbequi  1693  exlimdd  1725  exlimddv  1751  cbvaldva  1776  cbvexdva  1777  nfsbxyt  1792  sbcomxyyz  1819  nfsb4t  1863  eupickbi  1955  moexexdc  1957  euexex  1958  2euswapdc  1964  dvelimdc  2170  nebidc  2254  rgen2a  2344  ralimiaa  2352  ralimdaa  2355  ralrimiva  2361  ralrimdva  2368  ralrimivva  2370  ralrimdvv  2372  ralrimdvva  2373  reximdva  2390  rexlimiva  2397  rexlimdva  2402  rexlimdvva  2409  r19.29_2a  2425  2gencl  2555  vtocldf  2573  spcimdv  2605  spcimedv  2607  rspct  2617  eqvinc  2635  eqvincg  2636  ceqex  2639  reu6  2698  eqreu  2701  sbciedf  2766  rmob  2818  csbiebt  2854  csbiedf  2855  reupick  3189  reximdva0m  3204  ssn0  3227  rgenm  3291  preqr1g  3500  prel12  3505  dfnfc2  3561  intssunim  3600  intab  3607  iineq2d  3640  ssiun2  3663  mpteq2da  3809  trintssm  3833  copsexg  3944  copsex2t  3945  sess1  4031  sess2  4032  tron  4057  onelss  4062  onintss  4065  reusv1  4128  reusv3  4130  rabxfrd  4139  iunpw  4149  ssorduni  4151  ordsson  4156  ordsucg  4166  onsucelsucexmidlem  4186  elirr  4196  en2lp  4204  ordsuc  4213  ordpwsucss  4215  tfisi  4225  sosng  4328  2optocl  4332  relop  4401  xpid11m  4472  releldmb  4486  relelrnb  4487  elrnmptg  4501  elreimasng  4606  relbrcnvg  4619  trin2  4631  ssxpbm  4671  ssxp1  4672  ssxp2  4673  elxp4  4723  elxp5  4724  relresfld  4762  relcoi1  4764  iotaval  4793  iotass  4799  funmo  4831  imadif  4893  imain  4895  2elresin  4924  feu  4985  fcnvres  4986  f1oun  5059  f1oprg  5081  relfvssunirn  5104  funbrfv  5125  funbrfv2b  5131  dffn5im  5132  dfimafn  5135  funimass4  5137  ssimaex  5147  fvmptssdm  5168  fvmptf  5176  fvimacnv  5195  funimass3  5196  elpreima  5199  elrnrexdm  5219  eldmrexrn  5221  dffo4  5228  dffo5  5229  fmpt  5232  ffvresb  5241  fmptco  5243  fsn  5248  funfvima  5303  funfvima2  5304  f1mpt  5323  f1imass  5326  f1ocnvfvrneq  5335  foeqcnvco  5343  f1eqcocnv  5344  fliftfun  5349  fliftf  5352  isopolem  5374  isosolem  5376  eusvobj2  5410  acexmidlemab  5418  oprabid  5449  ovidi  5530  ovg  5550  suppssfv  5619  suppssov1  5620  funrnex  5652  f1dmex  5654  oprabexd  5665  fo2ndresm  5700  op1steq  5716  dfoprab3  5728  fo2ndf  5759  f1o2ndf1  5760  poxp  5763  isprmpt2  5768  reldmtpos  5778  rntpos  5782  tposf2  5793  tposf12  5794  issmo2  5814  smores  5817  smoiso  5827  tfrlem9  5845  tfrlemibacc  5849  tfrlemibfn  5851  tfrlemi14d  5856  tfrexlem  5858  rdgi0g  5874  rdgivallem  5876  frecsuclem3  5894  frecrdg  5896  oawordi  5952  nnmcom  5971  nnsucelsuc  5973  nntri3or  5975  nntri1  5977  nnaordi  5980  nnmord  5989  nnaordex  5999  nnm00  6001  ertr  6020  erex  6029  iserd  6031  iinerm  6077  erinxp  6079  qsel  6082  qliftfun  6087  qliftfund  6088  2ecoptocl  6093  brecop  6095  mulcanpig  6181  nlt1pig  6187  addcmpblnq  6212  ltsonq  6243  ltexnqq  6252  prarloclemarch2  6262  enq0tr  6275  addcmpblnq0  6284  addnq0mo  6288  mulnq0mo  6289  prcdnql  6324  prcunqu  6325  prarloclemlo  6334  prarloclem3step  6336  prarloclem3  6337  genpdflem  6347  genpelvl  6352  genpelvu  6353  genpcdl  6360  genpcuu  6361  genprndl  6362  genprndu  6363  genpdisj  6364  addnqprllem  6368  addnqprulem  6369  addlocprlemeq  6374  addlocprlemgt  6375  nqprloc  6386  prmuloc  6396  prmuloc2  6397  mullocpr  6401  distrlem4prl  6409  distrlem4pru  6410  ltprordil  6414  1idprl  6415  1idpru  6416  ltpopr  6418  ltsopr  6419  ltaddpr  6420  ltexprlemm  6423  ltexprlemlol  6425  ltexprlemupu  6427  ltexprlemdisj  6429  ltexprlemloc  6430  ltexprlemrl  6433  ltexprlemru  6435  addcanprleml  6437  addcanprlemu  6438  addcanprg  6439  ltaprg  6441  recexprlemlol  6447  recexprlemdisj  6451  recexprlemloc  6452  recexprlem1ssl  6454  recexprlem1ssu  6455  aptiprleml  6460  aptiprlemu  6461  ltmprr  6463  mulcmpblnrlemg  6478  addsrmo  6481  mulsrmo  6482  ltsrprg  6485  lelttr  6706  ltletr  6707  readdcan  6753  cnegexlem1  6786  cnegexlem2  6787  add20  7067  recexre  7165  inelr  7171  rimul  7172  apreap  7174  ltmul1  7179  cru  7189  apreim  7190  apirr  7192  apsym  7193  apcotr  7194  apadd1  7195  apneg  7198  mulext1  7199  msqge0  7203  mulge0  7206  apti  7209  ltleap  7216  recexap  7219  mulap0b  7221  recgt0  7399  prodgt02  7402  prodge02  7404  lemul12b  7410  lemul12a  7411  nnrecgt0  7534  addltmul  7739  nominpos  7740  elnnz  7829  peano2z  7854  zaddcllempos  7855  zaddcl  7858  zltnle  7862  zrevaddcl  7865  zdceq  7883  nn0lt2  7886  zextle  7895  peano5uzti  7910  uzind2  7914  fzind  7917  fnn0ind  7918  nn0ind-raph  7919  qapne  8056  qreccl  8057  qrevaddcl  8059  irradd  8061  irrmul  8062  cbvrald  8192  bdsepnft  8271  peano5set  8324  findset  8329  bj-omtrans  8340  bj-findis  8359  strcollnft  8364
  Copyright terms: Public domain W3C validator