MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  expcom Structured version   Visualization version   GIF version

Theorem expcom 414
Description: Exportation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
Hypothesis
Ref Expression
ex.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
expcom (𝜓 → (𝜑𝜒))

Proof of Theorem expcom
StepHypRef Expression
1 ex.1 . . 3 ((𝜑𝜓) → 𝜒)
21ex 413 . 2 (𝜑 → (𝜓𝜒))
32com12 32 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 208  df-an 397
This theorem is referenced by:  ancoms  459  pm3.21  472  sylan  580  animpimp2impd  840  4casesdan  1033  dedlema  1037  dedlemb  1038  sbiedvw  2095  cbval2vOLD  2355  cbval2OLD  2424  mo4  2643  2moswapv  2707  2moswap  2722  2mos  2727  2eu2  2731  pm2.61ne  3099  nelelne  3114  r19.21be  3207  cbvraldva2  3454  cbvrexdva2OLD  3456  rspcebdv  3614  2reu2  3879  minel  4411  uneqdifeq  4434  raltpd  4708  ssunsn2  4752  opthprneg  4787  ssuni  4852  uniss2  4862  elpwuni  5018  disjord  5045  elssabg  5230  elpw2g  5238  axprlem3  5316  axprlem4  5317  axprlem5  5318  oteqex  5381  otsndisj  5400  otiunsndisj  5401  epelg  5459  epelgOLD  5460  wereu  5544  relop  5714  riinint  5832  sotri3  5983  unixpid  6128  reuop  6137  ordtr2  6228  ordsssuc2  6272  iotan0  6338  funopg  6382  fun  6533  tz6.12c  6688  fvmptnf  6782  fvn0ssdmfun  6834  eldmrexrnb  6850  fmptco  6883  fnressn  6912  fressnfv  6914  fprb  6948  fvtp2g  6953  fvtp3g  6954  fconst2g  6957  fntpb  6963  f1dom3el3dif  7018  isores3  7077  isoselem  7083  oprabv  7203  eloprabga  7250  sorpsscmpl  7449  difex2  7471  ordpwsuc  7519  ordsucun  7529  limuni3  7556  ordom  7578  fo1stres  7704  poxp  7811  soxp  7812  suppimacnv  7830  frnsuppeq  7831  funsssuppss  7845  brtpos2  7887  wfrlem12  7955  onnseq  7970  smores  7978  smofvon2  7982  tfrlem1  8001  oacl  8149  omcl  8150  oecl  8151  oawordri  8165  oalimcl  8175  oaass  8176  oarec  8177  omwordri  8187  omeulem1  8197  omeulem2  8198  oeordi  8202  oeworde  8208  oeoelem  8213  nnacl  8226  nnmcl  8227  nnecl  8228  nnacom  8232  nnaass  8237  nnmsucr  8240  nnmordi  8246  omabs  8263  iiner  8358  elpmg  8411  pmss12g  8422  mapfvd  8432  f1domg  8517  ssdomg  8543  domtriord  8651  php  8689  php3  8691  1sdom  8709  fisseneq  8717  isinf  8719  ssnnfi  8725  dif1en  8739  findcard3  8749  frfi  8751  unfi  8773  difinf  8776  fnfi  8784  iunfi  8800  fsuppunfi  8841  fsuppres  8846  frnfsuppbi  8850  elfi2  8866  marypha1lem  8885  marypha1  8886  oiexg  8987  wemapso2  9005  harword  9017  brwdom  9019  unxpwdom  9041  en3lplem1  9063  inf3lemd  9078  inf3lem5  9083  cantnfval2  9120  cantnfle  9122  cantnflt  9123  cnfcom  9151  tcmin  9171  r1sdom  9191  rankxplim3  9298  cardidm  9376  cardmin2  9415  infxpenlem  9427  fseqenlem1  9438  numacn  9463  alephordi  9488  iscard3  9507  alephinit  9509  carduniima  9510  iunfictbso  9528  dfac5  9542  dfac12lem3  9559  pwsdompw  9614  pwdjudom  9626  cflim2  9673  cfslb2n  9678  cofsmo  9679  cfsmolem  9680  cfcoflem  9682  alephsing  9686  infpssALT  9723  fin23lem34  9756  isf32lem2  9764  isf32lem10  9772  isf32lem12  9774  isfin1-2  9795  hsmexlem4  9839  axcc2lem  9846  domtriomlem  9852  axdc2lem  9858  axdc3lem2  9861  axdc3lem4  9863  axdc4lem  9865  axcclem  9867  ac6num  9889  ac6s  9894  zorn2lem7  9912  ttukeylem5  9923  imadomg  9944  iundom2g  9950  ondomon  9973  ficard  9975  konigthlem  9978  alephreg  9992  pwcfsdom  9993  cfpwsdom  9994  axregndlem1  10012  axregnd  10014  pwfseqlem3  10070  pwxpndom2  10075  pwxpndom  10076  pwdjundom  10077  inawinalem  10099  gchina  10109  wuncval2  10157  tsk0  10173  tskxpss  10182  inatsk  10188  tskuni  10193  gruina  10228  grothac  10240  addclpi  10302  addnidpi  10311  nqereu  10339  mulcanenq  10370  genpnnp  10415  nqpr  10424  prlem934  10443  reclem2pr  10458  suplem1pr  10462  supsrlem  10521  axpre-sup  10579  1re  10629  dedekindle  10792  00id  10803  receu  11273  sup3  11586  infrelb  11614  peano5nni  11629  nnaddcl  11648  zrevaddcl  12015  nzadd  12018  zdiv  12040  nneo  12054  zeo2  12057  nn0indd  12067  fzind  12068  fnn0ind  12069  uzwo  12299  lbzbi  12324  nn01to3  12329  qrevaddcl  12358  irradd  12360  irrmul  12361  ltsubrp  12413  ltaddrp  12414  xnn0xaddcl  12616  xnn0xadd0  12628  icoshft  12847  fzen  12912  elfzm11  12966  uzsplit  12967  elfzoext  13082  elfzom1elp1fzo  13092  injresinjlem  13145  injresinj  13146  modifeq2int  13289  modsumfzodifsn  13300  om2uzlti  13306  ssnn0fi  13341  fsuppmapnn0fiub0  13349  mptnn0fsuppr  13355  seqcaopr3  13393  seqf1olem2a  13396  seqf1o  13399  ser1const  13414  expadd  13459  expmul  13462  leexp1a  13527  faccl  13631  facdiv  13635  faclbnd  13638  faclbnd4lem4  13644  hasheqf1oi  13700  hashgadd  13726  hashinfxadd  13734  hashunx  13735  hashunsng  13741  elprchashprn2  13745  hashss  13758  hash1snb  13768  hashmap  13784  hashf1lem2  13802  hashf1  13803  seqcoll  13810  hashle2pr  13823  hashdmpropge2  13829  hashge3el3dif  13832  hash1to3  13837  fundmge2nop0  13838  fi1uzind  13843  brfi1indALT  13846  sswrd  13857  swrdnd2  14005  swrdnnn0nd  14006  swrdnd0  14007  swrdwrdsymb  14012  pfxnd0  14038  swrdswrdlem  14054  swrdswrd  14055  wrd2ind  14073  swrdccatin1  14075  swrdccatin2  14079  pfxccatin12lem2  14081  pfxccat3  14084  repsdf2  14128  repswswrd  14134  cshw0  14144  cshwcl  14148  cshwlen  14149  cshf1  14160  swrdco  14187  relexpsucnnl  14379  rtrclreclem3  14407  rtrclreclem4  14408  relexpindlem  14410  rtrclind  14412  shftlem  14415  caubnd  14706  reusq0  14810  rlimcld2  14923  o1dif  14974  climub  15006  climserle  15007  iseraltlem2  15027  sumss  15069  fsumzcl2  15083  fsummsnunz  15097  fsumsplitsnun  15098  fsum2d  15114  modfsummods  15136  fsumabs  15144  fsumrlim  15154  fsumo1  15155  fsumiun  15164  climcndslem1  15192  climcndslem2  15193  cvgrat  15227  clim2prod  15232  prodfn0  15238  prodfrec  15239  ntrivcvg  15241  prodmo  15278  fprodss  15290  fprodabs  15316  fprodn0  15321  fprod2d  15323  fprodefsum  15436  ruclem8  15578  ruclem9  15579  dvdsmod0  15601  dvds2ln  15630  dvdsaddre2b  15645  dvdslelem  15647  dvdsdivcl  15654  alzdvds  15658  mod2eq1n2dvds  15684  oddnn02np1  15685  nn0o1gt2  15720  nno  15721  sumeven  15726  sumodd  15727  pwp1fsum  15730  ndvdsadd  15749  bitsinv1  15779  sadcadd  15795  sadadd2  15797  saddisjlem  15801  smuval2  15819  smupvallem  15820  smu01lem  15822  smupval  15825  smueqlem  15827  smumullem  15829  gcddiv  15887  gcdmultipleOLD  15888  rplpwr  15895  nn0seqcvgd  15902  seq1st  15903  alginv  15907  algcvga  15911  algfx  15912  absprodnn  15950  isprm2  16014  isprm3  16015  prmind2  16017  maxprmfct  16041  prmdvdsexp  16047  pcmpt  16216  prmreclem4  16243  vdwmc2  16303  vdwlem10  16314  ramub2  16338  ramcl  16353  prmgaplem5  16379  prmgaplem8  16382  cshwshashlem1  16417  cshwshashlem3  16419  setsn0fun  16508  imasleval  16802  divsfval  16808  mreexexlem4d  16906  isssc  17078  initoeu1  17259  termoeu1  17266  istos  17633  mgmcl  17843  sgrpidmnd  17904  frmdgsum  18015  dfgrp3lem  18135  mhmmulg  18206  resghm2b  18314  gsumwrev  18432  elsymgbas  18438  symgextf1  18478  gsmsymgreqlem2  18488  gsmsymgreq  18489  odlem1  18592  odcl2  18621  gexlem1  18633  efgi2  18780  efginvrel2  18782  efgsrel  18789  cyggexb  18948  gsummulglem  18990  gsumzunsnd  19005  gsum2dlem2  19020  telgsums  19042  dmdprd  19049  dprdw  19061  ablfac1eulem  19123  srgpcomp  19211  lmodfopnelem1  19599  rmodislmodlem  19630  mplcoe1  20174  mplcoe3  20175  mplcoe5  20177  cply1mul  20390  coe1fzgsumdlem  20397  gsummoncoe1  20400  pf1ind  20446  evl1gsumdlem  20447  cnfldmulg  20505  cnfldexp  20506  obslbs  20802  mat1dimcrng  21014  ma1repveval  21108  mulmarep1gsum2  21111  gsummatr01lem3  21194  cramerlem3  21226  decpmatmulsumfsupp  21309  mp2pm2mplem4  21345  pm2mpmhmlem1  21354  fvmptnn04if  21385  cayhamlem1  21402  fctop  21540  mretopd  21628  restopnb  21711  restdis  21714  tgcnp  21789  cncls2  21809  cncls  21810  cnntr  21811  cnsscnp  21815  cmpsub  21936  2ndcsep  21995  1stcelcls  21997  lfinpfin  22060  locfincmp  22062  comppfsc  22068  txcn  22162  txlm  22184  xkohaus  22189  qtopres  22234  haushmphlem  22323  cmphmph  22324  connhmph  22325  reghmph  22329  nrmhmph  22330  ptcmpfi  22349  reghaus  22361  fbssfi  22373  fbun  22376  fbfinnfr  22377  isfildlem  22393  fgcl  22414  cfinfil  22429  supfil  22431  ufinffr  22465  fin1aufil  22468  cnpflf  22537  alexsubALTlem3  22585  alexsubALT  22587  cnextfvval  22601  cnextcn  22603  tmdgsum  22631  tgphaus  22652  tgpt1  22653  mettri  22889  blssexps  22963  blssex  22964  mopni3  23031  metss  23045  psmetutop  23104  dscmet  23109  tngngp3  23192  rectbntr0  23367  metnrmlem1a  23393  fsumcn  23405  lmmbr  23788  caubl  23838  caublcls  23839  bcthlem5  23858  bcth3  23861  ovolunlem1a  24024  ovoliunnul  24035  finiunmbl  24072  voliunlem1  24078  volsuplem  24083  volsup  24084  dyadmax  24126  itgfsum  24354  dvnadd  24453  cpnord  24459  dvnfre  24476  dvmptfsum  24499  dvlip  24517  fta1g  24688  plyco  24758  dgrcolem1  24790  dgrco  24792  dvnply2  24803  plydivex  24813  plyexmo  24829  aannenlem1  24844  aaliou3lem2  24859  dvntaylp  24886  taylthlem1  24888  ulmval  24895  cxpmul2  25199  cxpsqrtth  25239  scvxcvx  25490  jensenlem2  25492  jensen  25493  ppiub  25707  bcmono  25780  bpos1lem  25785  bposlem5  25791  gausslemma2dlem6  25875  lgsquad2lem2  25888  2lgslem3  25907  2lgs  25910  2sqnn  25942  addsqnreup  25946  2sqreultblem  25951  2sqreunnltblem  25954  dchrisumlem1  25992  dchrisum0flb  26013  pntpbnd1  26089  pntlemf  26108  qabvle  26128  qabvexp  26129  ostthlem2  26131  ostth2lem2  26137  axeuclidlem  26675  axcontlem12  26688  umgrnloopv  26818  uhgredgrnv  26842  edglnl  26855  numedglnl  26856  usgruspgrb  26893  usgrnloopvALT  26910  usgredg2vlem2  26935  subupgr  26996  nbumgr  27056  uhgrnbgr0nb  27063  nbgr0vtxlem  27064  edgusgrnbfin  27082  nb3grprlem2  27090  uvtxnbgrvtx  27102  cplgrop  27146  cusgrfi  27167  fusgrmaxsize  27173  fusgrn0degnn0  27208  ewlkprop  27312  uspgr2wlkeq  27354  g0wlk0  27360  wlkreslem  27378  lfgriswlk  27397  upgrwlkdvde  27445  spthonepeq  27460  uhgrwkspth  27463  usgr2trlncl  27468  usgr2trlspth  27469  cyclnspth  27508  crctcshwlkn0lem3  27517  wwlksn  27542  wspthneq1eq2  27565  wwlksm1edg  27586  wwlksnred  27597  wwlksnextfun  27603  wwlksnextinj  27604  wwlksnextproplem3  27617  wspthsnonn0vne  27623  wspn0  27630  rusgrnumwwlk  27681  clwwlkccatlem  27694  umgrclwwlkge2  27696  clwlkclwwlklem2  27705  clwlkclwwlklem3  27706  clwwisshclwws  27720  clwwisshclwwsn  27721  clwwlkn1loopb  27748  clwwlknfiOLD  27751  wwlksext2clwwlk  27763  wwlksubclwwlk  27764  clwwlknonex2lem2  27814  upgr3v3e3cycl  27886  uhgr3cyclex  27888  upgr4cycl4dv4e  27891  eupth2lem3lem4  27937  eupth2lem3lem7  27940  eupth2  27945  eulerpath  27947  nfrgr2v  27978  frgr3vlem1  27979  3vfriswmgr  27984  1to2vfriswmgr  27985  1to3vfriswmgr  27986  3cyclfrgrrn1  27991  3cyclfrgrrn  27992  3cyclfrgrrn2  27993  4cycl2vnunb  27996  frgrncvvdeqlem2  28006  frgrncvvdeqlem8  28012  frgrncvvdeqlem9  28013  frgrwopreglem4a  28016  frgrwopreglem5lem  28026  frgrwopreglem5ALT  28028  frgrregorufr0  28030  frgr2wwlk1  28035  frgr2wwlkeqm  28037  fusgr2wsp2nb  28040  2wspmdisj  28043  frrusgrord  28047  numclwwlk1lem2f1  28063  numclwlk1  28077  frgrreggt1  28099  friendshipgt3  28104  hlim2  28896  elnlfn  29632  stle0i  29943  hstrbi  29970  spansncv2  29997  h1da  30053  fmptcof2  30330  nnindd  30462  xreceu  30525  tpr2rico  31054  hasheuni  31243  ismeas  31357  sseqp1  31552  rrvsum  31611  dstfrvunirn  31631  sgn3da  31698  signstfvc  31743  bnj607  32087  bnj1145  32162  bnj1204  32181  fisshasheq  32249  subgrwlk  32276  subfacp1lem6  32329  cvmlift2lem12  32458  cvmlift3lem4  32466  satfrnmapom  32514  sat1el2xp  32523  satffunlem2  32552  satffun  32553  mrsubvrs  32666  climuzcnv  32811  iprodefisumlem  32869  dfon2lem9  32933  trpredtr  32966  trpredmintr  32967  dftrpred3g  32969  trpredrec  32974  soseq  32993  frrlem8  33027  fpr2  33037  frr2  33042  sltval2  33060  sltsolem1  33077  linethru  33511  elhf2  33533  finminlem  33563  fnessref  33602  neibastop2lem  33605  fnemeet2  33612  nndivsub  33702  bj-xpnzex  34168  bj-elpwg  34239  bj-epelg  34254  bj-intss  34285  mptsnunlem  34501  dissneqlem  34503  topdifinffinlem  34510  iooelexlt  34525  domalom  34567  fvineqsneq  34575  wl-exeq  34655  wl-ax11-lem3  34700  matunitlindflem1  34769  poimirlem22  34795  poimirlem26  34799  poimirlem28  34801  poimirlem29  34802  poimirlem32  34805  heicant  34808  ovoliunnfl  34815  voliunnfl  34817  volsupnfl  34818  cover2  34870  upixp  34885  sdclem2  34898  fdc  34901  seqpo  34903  metf1o  34911  mettrifi  34913  sstotbnd3  34935  heibor1lem  34968  heiborlem5  34974  heibor  34980  bfplem1  34981  elghomlem2OLD  35045  grpokerinj  35052  isrngo  35056  rngodm1dm2  35091  ispridl2  35197  exlimddvf  35280  lssatle  36031  4atexlemex4  37089  sn-axprlem3  38987  mzpsubst  39223  jm2.18  39463  wepwsolem  39520  iunrelexp0  39925  relexpmulg  39933  cnvtrclfv  39947  clsk1indlem3  40271  grucollcld  40473  inaex  40510  dvgrat  40521  radcnvrat  40523  csbxpgVD  41105  sineq0ALT  41148  islptre  41776  iblspltprt  42134  stoweidlem2  42164  stoweidlem17  42179  stoweidlem21  42183  2reuimp0  43190  2reuimp  43191  afveu  43229  funbrafv  43234  ndmaovass  43282  afv2eu  43314  tz6.12c-afv2  43318  funop1  43359  f1oresf1o2  43367  fvmptrabdm  43369  nltle2tri  43390  2elfz2melfz  43395  fzoopth  43404  fsummsndifre  43409  fsumsplitsndif  43410  fsummmodsndifre  43411  fsummmodsnunz  43412  elsetpreimafvssdm  43423  uniimaelsetpreimafv  43433  imasetpreimafvbijlemfv1  43440  iccpartiltu  43459  iccpartigtl  43460  iccpartleu  43465  iccpartgel  43466  iccpartrn  43467  iccpartiun  43471  icceuelpart  43473  iccpartnel  43475  fargshiftf  43477  fargshiftf1  43478  ichnfb  43502  elsprel  43514  prsprel  43526  sprsymrelfo  43536  paireqne  43550  sbcpr  43560  reupr  43561  fmtnoinf  43575  odz2prm2pw  43602  lighneallem4  43652  lighneal  43653  requad1  43664  requad2  43665  evensumeven  43749  even3prm2  43761  gbowgt5  43804  nnsum4primeseven  43842  nnsum4primesevenALTV  43843  bgoldbnnsum3prm  43846  bgoldbtbndlem2  43848  bgoldbtbndlem4  43850  bgoldbtbnd  43851  isomuspgrlem1  43869  smndex1mgm  44007  clcllaw  44026  nrhmzr  44072  rnghmmul  44099  rngccatidALTV  44188  ringccatidALTV  44251  nzerooringczr  44271  scmsuppss  44348  gsumlsscl  44359  ply1mulgsumlem2  44369  lincvalsc0  44404  linc0scn0  44406  lincdifsn  44407  linc1  44408  lincellss  44409  lincsum  44412  lincscm  44413  lincsumcl  44414  lcoss  44419  lincext3  44439  lindslinindimp2lem4  44444  lindslinindsimp2lem5  44445  lindslinindsimp2  44446  lindsrng01  44451  snlindsntor  44454  lincresunit3lem2  44463  lincresunit3  44464  islindeps2  44466  blengt1fldiv2p1  44581  resum2sqorgt0  44624  reorelicc  44625  rrx2plordisom  44638  rrx2linest  44657  rrxsphere  44663  line2ylem  44666  itsclc0xyqsol  44683  itscnhlinecirc02p  44700
  Copyright terms: Public domain W3C validator