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

Theorem expcom 417
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 416 . 2 (𝜑 → (𝜓𝜒))
32com12 32 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  ancoms  462  pm3.21  475  sylan  583  animpimp2impd  843  4casesdan  1037  dedlema  1041  dedlemb  1042  sbiedvw  2105  cbval2vOLD  2365  cbval2OLD  2434  mo4  2650  2moswapv  2714  2moswap  2729  2mos  2734  2eu2  2737  pm2.61ne  3092  nelelne  3105  r19.21be  3198  cbvraldva2  3433  cbvrexdva2OLD  3435  rspcebdv  3594  2reu2  3856  csbie2df  4365  minel  4388  uneqdifeq  4411  raltpd  4689  ssunsn2  4733  opthprneg  4768  ssuni  4836  uniss2  4844  elpwuni  5000  disjord  5027  elssabg  5212  elpw2g  5220  axprlem3  5299  axprlem4  5300  axprlem5  5301  oteqex  5363  otsndisj  5382  otiunsndisj  5383  epelg  5439  epelgOLD  5440  wereu  5524  relop  5694  riinint  5812  sotri3  5963  unixpid  6108  reuop  6117  ordtr2  6208  ordsssuc2  6252  iotan0  6318  funopg  6362  fun  6513  tz6.12c  6668  fvmptnf  6763  fvn0ssdmfun  6815  eldmrexrnb  6831  fmptco  6864  fnressn  6893  fressnfv  6895  fprb  6929  fvtp2g  6934  fvtp3g  6935  fconst2g  6938  fntpb  6945  f1dom3el3dif  7001  isores3  7062  isoselem  7068  oprabv  7188  eloprabga  7235  sorpsscmpl  7435  difex2  7457  ordpwsuc  7505  ordsucun  7515  limuni3  7542  ordom  7564  fo1stres  7690  poxp  7797  soxp  7798  suppimacnv  7816  frnsuppeq  7817  funsssuppss  7831  brtpos2  7873  wfrlem12  7941  onnseq  7956  smores  7964  smofvon2  7968  tfrlem1  7987  oacl  8135  omcl  8136  oecl  8137  oawordri  8151  oalimcl  8161  oaass  8162  oarec  8163  omwordri  8173  omeulem1  8183  omeulem2  8184  oeordi  8188  oeworde  8194  oeoelem  8199  nnacl  8212  nnmcl  8213  nnecl  8214  nnacom  8218  nnaass  8223  nnmsucr  8226  nnmordi  8232  omabs  8249  iiner  8344  elpmg  8397  pmss12g  8408  mapfvd  8418  f1domg  8504  ssdomg  8530  domtriord  8639  php  8677  php3  8679  1sdom  8697  fisseneq  8705  isinf  8707  ssnnfi  8713  dif1en  8727  findcard3  8737  frfi  8739  unfi  8761  difinf  8764  fnfi  8772  iunfi  8788  fsuppunfi  8829  fsuppres  8834  frnfsuppbi  8838  elfi2  8854  marypha1lem  8873  marypha1  8874  oiexg  8975  wemapso2  8993  harword  9003  brwdom  9007  unxpwdom  9029  en3lplem1  9051  inf3lemd  9066  inf3lem5  9071  cantnfval2  9108  cantnfle  9110  cantnflt  9111  cnfcom  9139  tcmin  9159  r1sdom  9179  rankxplim3  9286  cardidm  9364  cardmin2  9404  infxpenlem  9416  fseqenlem1  9427  numacn  9452  alephordi  9477  iscard3  9496  alephinit  9498  carduniima  9499  iunfictbso  9517  dfac5  9531  dfac12lem3  9548  pwsdompw  9603  pwdjudom  9615  cflim2  9662  cfslb2n  9667  cofsmo  9668  cfsmolem  9669  cfcoflem  9671  alephsing  9675  infpssALT  9712  fin23lem34  9745  isf32lem2  9753  isf32lem10  9761  isf32lem12  9763  isfin1-2  9784  hsmexlem4  9828  axcc2lem  9835  domtriomlem  9841  axdc2lem  9847  axdc3lem2  9850  axdc3lem4  9852  axdc4lem  9854  axcclem  9856  ac6num  9878  ac6s  9883  zorn2lem7  9901  ttukeylem5  9912  imadomg  9933  iundom2g  9939  ondomon  9962  ficard  9964  konigthlem  9967  alephreg  9981  pwcfsdom  9982  cfpwsdom  9983  axregndlem1  10001  axregnd  10003  pwfseqlem3  10059  pwxpndom2  10064  pwxpndom  10065  pwdjundom  10066  inawinalem  10088  gchina  10098  wuncval2  10146  tsk0  10162  tskxpss  10171  inatsk  10177  tskuni  10182  gruina  10217  grothac  10229  addclpi  10291  addnidpi  10300  nqereu  10328  mulcanenq  10359  genpnnp  10404  nqpr  10413  prlem934  10432  reclem2pr  10447  suplem1pr  10451  supsrlem  10510  axpre-sup  10568  1re  10618  dedekindle  10781  00id  10792  receu  11262  sup3  11575  infrelb  11603  peano5nni  11618  nnindd  11635  nnaddcl  11638  zrevaddcl  12005  nzadd  12008  zdiv  12030  nneo  12044  zeo2  12047  nn0indd  12057  fzind  12058  fnn0ind  12059  uzwo  12289  lbzbi  12314  nn01to3  12319  qrevaddcl  12348  irradd  12350  irrmul  12351  ltsubrp  12403  ltaddrp  12404  xnn0xaddcl  12606  xnn0xadd0  12618  icoshft  12841  fzen  12907  elfzm11  12961  uzsplit  12962  elfzoext  13077  elfzom1elp1fzo  13087  injresinjlem  13140  injresinj  13141  modifeq2int  13284  modsumfzodifsn  13295  om2uzlti  13301  ssnn0fi  13336  fsuppmapnn0fiub0  13344  mptnn0fsuppr  13350  seqcaopr3  13389  seqf1olem2a  13392  seqf1o  13395  ser1const  13410  expadd  13455  expmul  13458  leexp1a  13523  faccl  13627  facdiv  13631  faclbnd  13634  faclbnd4lem4  13640  hasheqf1oi  13696  hashgadd  13722  hashinfxadd  13730  hashunx  13731  hashunsng  13737  elprchashprn2  13741  hashss  13754  hash1snb  13764  hashmap  13780  hashf1lem2  13798  hashf1  13799  seqcoll  13806  hashle2pr  13819  hashdmpropge2  13825  hashge3el3dif  13828  hash1to3  13833  fundmge2nop0  13834  fi1uzind  13839  brfi1indALT  13842  sswrd  13853  swrdnd2  13996  swrdnnn0nd  13997  swrdnd0  13998  swrdwrdsymb  14003  pfxnd0  14029  swrdswrdlem  14045  swrdswrd  14046  wrd2ind  14064  swrdccatin1  14066  swrdccatin2  14070  pfxccatin12lem2  14072  pfxccat3  14075  repsdf2  14119  repswswrd  14125  cshw0  14135  cshwcl  14139  cshwlen  14140  cshf1  14151  swrdco  14178  relexpsucnnl  14370  rtrclreclem3  14398  rtrclreclem4  14399  relexpindlem  14401  rtrclind  14403  shftlem  14406  caubnd  14697  reusq0  14801  rlimcld2  14914  o1dif  14965  climub  14997  climserle  14998  iseraltlem2  15018  sumss  15060  fsumzcl2  15074  fsummsnunz  15088  fsumsplitsnun  15089  fsum2d  15105  modfsummods  15127  fsumabs  15135  fsumrlim  15145  fsumo1  15146  fsumiun  15155  climcndslem1  15183  climcndslem2  15184  cvgrat  15218  clim2prod  15223  prodfn0  15229  prodfrec  15230  ntrivcvg  15232  prodmo  15269  fprodss  15281  fprodabs  15307  fprodn0  15312  fprod2d  15314  fprodefsum  15427  ruclem8  15569  ruclem9  15570  dvdsmod0  15592  dvds2ln  15621  dvdsaddre2b  15636  dvdslelem  15638  dvdsdivcl  15645  alzdvds  15649  mod2eq1n2dvds  15675  oddnn02np1  15676  nn0o1gt2  15709  nno  15710  sumeven  15715  sumodd  15716  pwp1fsum  15719  ndvdsadd  15738  bitsinv1  15768  sadcadd  15784  sadadd2  15786  saddisjlem  15790  smuval2  15808  smupvallem  15809  smu01lem  15811  smupval  15814  smueqlem  15816  smumullem  15818  gcddiv  15876  gcdmultipleOLD  15877  rplpwr  15884  nn0seqcvgd  15891  seq1st  15892  alginv  15896  algcvga  15900  algfx  15901  absprodnn  15939  isprm2  16003  isprm3  16004  prmind2  16006  maxprmfct  16030  prmdvdsexp  16036  pcmpt  16205  prmreclem4  16232  vdwmc2  16292  vdwlem10  16303  ramub2  16327  ramcl  16342  prmgaplem5  16368  prmgaplem8  16371  cshwshashlem1  16408  cshwshashlem3  16410  setsn0fun  16499  imasleval  16793  divsfval  16799  mreexexlem4d  16897  isssc  17069  initoeu1  17250  termoeu1  17257  istos  17624  mgmcl  17834  sgrpidmnd  17895  frmdgsum  18006  smndex1mgm  18051  dfgrp3lem  18176  mhmmulg  18247  resghm2b  18355  gsumwrev  18473  elsymgbas  18481  symgextf1  18528  gsmsymgreqlem2  18538  gsmsymgreq  18539  odlem1  18642  odcl2  18671  gexlem1  18683  efgi2  18830  efginvrel2  18832  efgsrel  18839  cyggexb  18998  gsummulglem  19040  gsumzunsnd  19055  gsum2dlem2  19070  telgsums  19092  dmdprd  19099  dprdw  19111  ablfac1eulem  19173  srgpcomp  19261  lmodfopnelem1  19646  rmodislmodlem  19677  mplcoe1  20222  mplcoe3  20223  mplcoe5  20225  cply1mul  20438  coe1fzgsumdlem  20445  gsummoncoe1  20448  pf1ind  20494  evl1gsumdlem  20495  cnfldmulg  20553  cnfldexp  20554  obslbs  20850  mat1dimcrng  21062  ma1repveval  21156  mulmarep1gsum2  21159  gsummatr01lem3  21242  cramerlem3  21274  decpmatmulsumfsupp  21357  mp2pm2mplem4  21393  pm2mpmhmlem1  21402  fvmptnn04if  21433  cayhamlem1  21450  fctop  21588  mretopd  21676  restopnb  21759  restdis  21762  tgcnp  21837  cncls2  21857  cncls  21858  cnntr  21859  cnsscnp  21863  cmpsub  21984  2ndcsep  22043  1stcelcls  22045  lfinpfin  22108  locfincmp  22110  comppfsc  22116  txcn  22210  txlm  22232  xkohaus  22237  qtopres  22282  haushmphlem  22371  cmphmph  22372  connhmph  22373  reghmph  22377  nrmhmph  22378  ptcmpfi  22397  reghaus  22409  fbssfi  22421  fbun  22424  fbfinnfr  22425  isfildlem  22441  fgcl  22462  cfinfil  22477  supfil  22479  ufinffr  22513  fin1aufil  22516  cnpflf  22585  alexsubALTlem3  22633  alexsubALT  22635  cnextfvval  22649  cnextcn  22651  tmdgsum  22679  tgphaus  22701  tgpt1  22702  mettri  22938  blssexps  23012  blssex  23013  mopni3  23080  metss  23094  psmetutop  23153  dscmet  23158  tngngp3  23241  rectbntr0  23416  metnrmlem1a  23442  fsumcn  23454  lmmbr  23841  caubl  23891  caublcls  23892  bcthlem5  23911  bcth3  23914  ovolunlem1a  24079  ovoliunnul  24090  finiunmbl  24127  voliunlem1  24133  volsuplem  24138  volsup  24139  dyadmax  24181  itgfsum  24409  dvnadd  24511  cpnord  24517  dvnfre  24534  dvmptfsum  24557  dvlip  24575  fta1g  24747  plyco  24817  dgrcolem1  24849  dgrco  24851  dvnply2  24862  plydivex  24872  plyexmo  24888  aannenlem1  24903  aaliou3lem2  24918  dvntaylp  24945  taylthlem1  24947  ulmval  24954  cxpmul2  25259  cxpsqrtth  25299  scvxcvx  25550  jensenlem2  25552  jensen  25553  ppiub  25767  bcmono  25840  bpos1lem  25845  bposlem5  25851  gausslemma2dlem6  25935  lgsquad2lem2  25948  2lgslem3  25967  2lgs  25970  2sqnn  26002  addsqnreup  26006  2sqreultblem  26011  2sqreunnltblem  26014  dchrisumlem1  26052  dchrisum0flb  26073  pntpbnd1  26149  pntlemf  26168  qabvle  26188  qabvexp  26189  ostthlem2  26191  ostth2lem2  26197  axeuclidlem  26735  axcontlem12  26748  umgrnloopv  26878  uhgredgrnv  26902  edglnl  26915  numedglnl  26916  usgruspgrb  26953  usgrnloopvALT  26970  usgredg2vlem2  26995  subupgr  27056  nbumgr  27116  uhgrnbgr0nb  27123  nbgr0vtxlem  27124  edgusgrnbfin  27142  nb3grprlem2  27150  uvtxnbgrvtx  27162  cplgrop  27206  cusgrfi  27227  fusgrmaxsize  27233  fusgrn0degnn0  27268  ewlkprop  27372  uspgr2wlkeq  27414  g0wlk0  27420  wlkreslem  27438  lfgriswlk  27457  upgrwlkdvde  27505  spthonepeq  27520  uhgrwkspth  27523  usgr2trlncl  27528  usgr2trlspth  27529  cyclnspth  27568  crctcshwlkn0lem3  27577  wwlksn  27602  wspthneq1eq2  27625  wwlksm1edg  27646  wwlksnred  27657  wwlksnextfun  27663  wwlksnextinj  27664  wwlksnextproplem3  27676  wspthsnonn0vne  27682  wspn0  27689  rusgrnumwwlk  27740  clwwlkccatlem  27753  umgrclwwlkge2  27755  clwlkclwwlklem2  27764  clwlkclwwlklem3  27765  clwwisshclwws  27779  clwwisshclwwsn  27780  clwwlkn1loopb  27807  wwlksext2clwwlk  27821  wwlksubclwwlk  27822  clwwlknonex2lem2  27872  upgr3v3e3cycl  27944  uhgr3cyclex  27946  upgr4cycl4dv4e  27949  eupth2lem3lem4  27995  eupth2lem3lem7  27998  eupth2  28003  eulerpath  28005  nfrgr2v  28036  frgr3vlem1  28037  3vfriswmgr  28042  1to2vfriswmgr  28043  1to3vfriswmgr  28044  3cyclfrgrrn1  28049  3cyclfrgrrn  28050  3cyclfrgrrn2  28051  4cycl2vnunb  28054  frgrncvvdeqlem2  28064  frgrncvvdeqlem8  28070  frgrncvvdeqlem9  28071  frgrwopreglem4a  28074  frgrwopreglem5lem  28084  frgrwopreglem5ALT  28086  frgrregorufr0  28088  frgr2wwlk1  28093  frgr2wwlkeqm  28095  fusgr2wsp2nb  28098  2wspmdisj  28101  frrusgrord  28105  numclwwlk1lem2f1  28121  numclwlk1  28135  frgrreggt1  28157  friendshipgt3  28162  hlim2  28954  elnlfn  29690  stle0i  30001  hstrbi  30028  spansncv2  30055  h1da  30111  fmptcof2  30389  xreceu  30585  tpr2rico  31163  hasheuni  31352  ismeas  31466  sseqp1  31661  rrvsum  31720  dstfrvunirn  31740  sgn3da  31807  signstfvc  31852  bnj607  32196  bnj1145  32273  bnj1204  32292  fisshasheq  32360  subgrwlk  32387  subfacp1lem6  32440  cvmlift2lem12  32569  cvmlift3lem4  32577  satfrnmapom  32625  sat1el2xp  32634  satffunlem2  32663  satffun  32664  mrsubvrs  32777  climuzcnv  32922  iprodefisumlem  32980  dfon2lem9  33044  trpredtr  33077  trpredmintr  33078  dftrpred3g  33080  trpredrec  33085  soseq  33104  frrlem8  33138  fpr2  33148  frr2  33153  sltval2  33171  sltsolem1  33188  linethru  33622  elhf2  33644  finminlem  33674  fnessref  33713  neibastop2lem  33716  fnemeet2  33723  nndivsub  33813  bj-xpnzex  34289  bj-elpwg  34363  bj-epelg  34378  bj-intss  34409  mptsnunlem  34639  dissneqlem  34641  topdifinffinlem  34648  iooelexlt  34663  domalom  34705  fvineqsneq  34713  wl-exeq  34821  wl-ax11-lem3  34866  matunitlindflem1  34935  poimirlem22  34961  poimirlem26  34965  poimirlem28  34967  poimirlem29  34968  poimirlem32  34971  heicant  34974  ovoliunnfl  34981  voliunnfl  34983  volsupnfl  34984  cover2  35034  upixp  35049  sdclem2  35062  fdc  35065  seqpo  35067  metf1o  35075  mettrifi  35077  sstotbnd3  35096  heibor1lem  35129  heiborlem5  35135  heibor  35141  bfplem1  35142  elghomlem2OLD  35206  grpokerinj  35213  isrngo  35217  rngodm1dm2  35252  ispridl2  35358  exlimddvf  35441  lssatle  36193  4atexlemex4  37251  fzindd  39145  sn-axprlem3  39235  mzpsubst  39496  jm2.18  39736  wepwsolem  39793  iunrelexp0  40210  relexpmulg  40218  cnvtrclfv  40232  clsk1indlem3  40556  grucollcld  40779  inaex  40816  dvgrat  40827  radcnvrat  40829  csbxpgVD  41411  sineq0ALT  41454  islptre  42080  iblspltprt  42434  stoweidlem2  42463  stoweidlem17  42478  stoweidlem21  42482  2reuimp0  43489  2reuimp  43490  afveu  43528  funbrafv  43533  ndmaovass  43581  afv2eu  43613  tz6.12c-afv2  43617  funop1  43658  f1oresf1o2  43666  fvmptrabdm  43668  nltle2tri  43689  2elfz2melfz  43694  fzoopth  43703  fsummsndifre  43708  fsumsplitsndif  43709  fsummmodsndifre  43710  fsummmodsnunz  43711  elsetpreimafvssdm  43722  uniimaelsetpreimafv  43732  imasetpreimafvbijlemfv1  43739  iccpartiltu  43758  iccpartigtl  43759  iccpartleu  43764  iccpartgel  43765  iccpartrn  43766  iccpartiun  43770  icceuelpart  43772  iccpartnel  43774  fargshiftf  43776  fargshiftf1  43777  ichnfb  43801  elsprel  43811  prsprel  43823  sprsymrelfo  43833  paireqne  43847  sbcpr  43857  reupr  43858  fmtnoinf  43872  odz2prm2pw  43899  lighneallem4  43947  lighneal  43948  requad1  43959  requad2  43960  evensumeven  44044  even3prm2  44056  gbowgt5  44099  nnsum4primeseven  44137  nnsum4primesevenALTV  44138  bgoldbnnsum3prm  44141  bgoldbtbndlem2  44143  bgoldbtbndlem4  44145  bgoldbtbnd  44146  isomuspgrlem1  44164  clcllaw  44270  nrhmzr  44316  rnghmmul  44343  rngccatidALTV  44432  ringccatidALTV  44495  nzerooringczr  44515  scmsuppss  44592  gsumlsscl  44603  ply1mulgsumlem2  44613  lincvalsc0  44648  linc0scn0  44650  lincdifsn  44651  linc1  44652  lincellss  44653  lincsum  44656  lincscm  44657  lincsumcl  44658  lcoss  44663  lincext3  44683  lindslinindimp2lem4  44688  lindslinindsimp2lem5  44689  lindslinindsimp2  44690  lindsrng01  44695  snlindsntor  44698  lincresunit3lem2  44707  lincresunit3  44708  islindeps2  44710  blengt1fldiv2p1  44825  resum2sqorgt0  44930  reorelicc  44931  rrx2plordisom  44944  rrx2linest  44963  rrxsphere  44969  line2ylem  44972  itsclc0xyqsol  44989  itscnhlinecirc02p  45006
  Copyright terms: Public domain W3C validator