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

Theorem expcom 451
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 450 . 2 (𝜑 → (𝜓𝜒))
32com12 32 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  ancoms  469  syldan  487  sylan  488  4casesdan  990  dedlema  1001  dedlemb  1002  cbval2  2277  cbvaldva  2279  2moswap  2545  2eu2  2552  pm2.61ne  2876  nelelne  2889  r19.21be  2930  rspcebdv  3309  minel  4024  uneqdifeq  4048  uneqdifeqOLD  4049  raltpd  4306  ssunsn2  4350  ssuni  4450  ssuniOLD  4451  uniss2  4461  elpwuni  4607  disjord  4632  elssabg  4810  elpw2g  4818  oteqex  4954  otsndisj  4969  otiunsndisj  4970  epelg  5020  wereu  5100  relop  5261  riinint  5371  sotri3  5514  unixpid  5658  ordtr2  5756  ordsssuc2  5802  funopg  5910  fun  6053  tz6.12c  6200  fvmptnf  6288  fvn0ssdmfun  6336  eldmrexrnb  6352  fmptco  6382  funopsn  6398  fnressn  6410  fressnfv  6412  fvtp2g  6449  fvtp3g  6450  fconst2g  6453  fntpb  6458  f1dom3el3dif  6511  isores3  6570  isoselem  6576  oprabv  6688  eloprabga  6732  sorpsscmpl  6933  difex2  6954  ordpwsuc  7000  ordsucun  7010  limuni3  7037  ordom  7059  fo1stres  7177  poxp  7274  soxp  7275  suppimacnv  7291  frnsuppeq  7292  funsssuppss  7306  brtpos2  7343  wfrlem12  7411  onnseq  7426  smores  7434  smofvon2  7438  tfrlem1  7457  oacl  7600  omcl  7601  oecl  7602  oawordri  7615  oalimcl  7625  oaass  7626  oarec  7627  omwordri  7637  omeulem1  7647  omeulem2  7648  oeordi  7652  oeworde  7658  oeoelem  7663  nnacl  7676  nnmcl  7677  nnecl  7678  nnacom  7682  nnaass  7687  nnmsucr  7690  nnmordi  7696  omabs  7712  iiner  7804  elpmg  7858  pmss12g  7869  mapsn  7884  f1domg  7960  ssdomg  7986  domtriord  8091  php  8129  php3  8131  1sdom  8148  fisseneq  8156  isinf  8158  ssnnfi  8164  dif1en  8178  findcard3  8188  frfi  8190  unfi  8212  difinf  8215  fnfi  8223  iunfi  8239  fsuppunfi  8280  fsuppres  8285  frnfsuppbi  8289  elfi2  8305  marypha1lem  8324  marypha1  8325  oiexg  8425  wemapso2  8443  harword  8455  brwdom  8457  unxpwdom  8479  en3lplem1  8496  inf3lemd  8509  inf3lem5  8514  cantnfval2  8551  cantnfle  8553  cantnflt  8554  cnfcom  8582  tcmin  8602  r1sdom  8622  rankxplim3  8729  cardidm  8770  cardmin2  8809  infxpenlem  8821  fseqenlem1  8832  numacn  8857  alephordi  8882  iscard3  8901  alephinit  8903  carduniima  8904  iunfictbso  8922  dfac5  8936  dfac12lem3  8952  pwsdompw  9011  pwcdadom  9023  cflim2  9070  cfslb2n  9075  cofsmo  9076  cfsmolem  9077  cfcoflem  9079  alephsing  9083  infpssALT  9120  fin23lem34  9153  isf32lem2  9161  isf32lem10  9169  isf32lem12  9171  isfin1-2  9192  hsmexlem4  9236  axcc2lem  9243  domtriomlem  9249  axdc2lem  9255  axdc3lem2  9258  axdc3lem4  9260  axdc4lem  9262  axcclem  9264  ac6num  9286  ac6s  9291  zorn2lem7  9309  ttukeylem5  9320  imadomg  9341  iundom2g  9347  ondomon  9370  ficard  9372  konigthlem  9375  alephreg  9389  pwcfsdom  9390  cfpwsdom  9391  axregndlem1  9409  axregnd  9411  pwfseqlem3  9467  pwxpndom2  9472  pwxpndom  9473  pwcdandom  9474  inawinalem  9496  gchina  9506  wuncval2  9554  tsk0  9570  tskxpss  9579  inatsk  9585  tskuni  9590  gruina  9625  grothac  9637  addclpi  9699  addnidpi  9708  nqereu  9736  mulcanenq  9767  genpnnp  9812  nqpr  9821  prlem934  9840  reclem2pr  9855  suplem1pr  9859  supsrlem  9917  axpre-sup  9975  1re  10024  dedekindle  10186  00id  10196  receu  10657  sup3  10965  infrelb  10993  peano5nni  11008  nnaddcl  11027  zrevaddcl  11407  nzadd  11410  zdiv  11432  nneo  11446  zeo2  11449  nn0indd  11459  fzind  11460  fnn0ind  11461  uzwo  11736  lbzbi  11761  nn01to3  11766  qrevaddcl  11795  irradd  11797  irrmul  11798  ltsubrp  11851  ltaddrp  11852  xnn0xaddcl  12051  xnn0xadd0  12062  icoshft  12279  fzen  12343  elfzm11  12395  uzsplit  12396  elfzoext  12508  elfzom1elp1fzo  12518  injresinjlem  12571  injresinj  12572  modifeq2int  12715  modsumfzodifsn  12726  om2uzlti  12732  ssnn0fi  12767  fsuppmapnn0fiub0  12776  mptnn0fsuppr  12782  seqcl2  12802  seqfveq2  12806  seqshft2  12810  monoord  12814  seqsplit  12817  seqcaopr3  12819  seqf1olem2a  12822  seqf1o  12825  seqid2  12830  seqhomo  12831  ser1const  12840  expadd  12885  expmul  12888  leexp1a  12902  faccl  13053  facdiv  13057  faclbnd  13060  faclbnd4lem4  13066  faclbnd6  13069  hasheqf1oi  13123  hasheqf1oiOLD  13124  hashf1rnOLD  13126  hashgadd  13149  hashinfxadd  13157  hashunx  13158  hashunsng  13164  elprchashprn2  13167  hashss  13180  hash1snb  13190  hashmap  13205  hashf1lem2  13223  hashf1  13224  seqcoll  13231  hashle2pr  13242  hashdmpropge2  13248  hashge3el3dif  13251  hash1to3  13256  fundmge2nop0  13257  fi1uzind  13262  brfi1indALT  13265  fi1uzindOLD  13268  brfi1indALTOLD  13271  sswrd  13296  swrdnd2  13415  swrdswrdlem  13441  swrdswrd  13442  wrd2ind  13459  swrdccatin1  13464  swrdccatin2  13468  swrdccatin12lem2  13470  swrdccat3  13473  repsdf2  13506  repswswrd  13512  cshw0  13521  cshwcl  13525  cshwlen  13526  cshf1  13537  swrdco  13564  relexpsucnnl  13753  rtrclreclem3  13781  rtrclreclem4  13782  relexpindlem  13784  rtrclind  13786  shftlem  13789  caubnd  14079  rlimcld2  14290  o1dif  14341  climub  14373  climserle  14374  iseraltlem2  14394  sumss  14436  fsumzcl2  14450  fsummsnunz  14464  fsumsplitsnun  14465  fsummsnunzOLD  14466  fsumsplitsnunOLD  14467  fsum2d  14483  modfsummods  14506  fsumabs  14514  fsumrlim  14524  fsumo1  14525  fsumiun  14534  bcxmas  14548  climcndslem1  14562  climcndslem2  14563  cvgrat  14596  clim2prod  14601  prodfn0  14607  prodfrec  14608  ntrivcvg  14610  prodmo  14647  fprodss  14659  fprodabs  14685  fprodn0  14690  fprod2d  14692  fprodefsum  14806  ruclem8  14947  ruclem9  14948  dvds2ln  14995  dvdsaddre2b  15010  dvdslelem  15012  dvdsdivcl  15019  alzdvds  15023  mod2eq1n2dvds  15052  oddnn02np1  15053  nn0o1gt2  15078  nno  15079  sumeven  15091  sumodd  15092  pwp1fsum  15095  ndvdsadd  15115  bitsinv1  15145  sadcadd  15161  sadadd2  15163  saddisjlem  15167  smuval2  15185  smupvallem  15186  smu01lem  15188  smupval  15191  smueqlem  15193  smumullem  15195  gcddiv  15249  gcdmultiple  15250  rplpwr  15257  nn0seqcvgd  15264  seq1st  15265  alginv  15269  algcvga  15273  algfx  15274  absprodnn  15312  isprm2  15376  isprm3  15377  prmind2  15379  maxprmfct  15402  prmdvdsexp  15408  pcmpt  15577  prmreclem4  15604  vdwmc2  15664  vdwlem10  15675  ramub2  15699  ramcl  15714  prmgaplem5  15740  prmgaplem8  15743  cshwshashlem1  15783  cshwshashlem3  15785  setsn0fun  15876  imasleval  16182  divsfval  16188  mreexexlem4d  16288  isssc  16461  initoeu1  16642  termoeu1  16649  istos  17016  mgmcl  17226  frmdgsum  17380  dfgrp3lem  17494  mhmmulg  17564  resghm2b  17659  gsumwrev  17777  elsymgbas  17783  symgextf1  17822  gsmsymgreqlem2  17832  gsmsymgreq  17833  odlem1  17935  odcl2  17963  gexlem1  17975  sylow1lem1  17994  efgi2  18119  efginvrel2  18121  efgsrel  18128  cyggexb  18281  gsummulglem  18322  gsumzunsnd  18336  gsum2dlem2  18351  telgsums  18371  dmdprd  18378  dprdw  18390  ablfac1eulem  18452  srgpcomp  18513  lmodfopnelem1  18880  rmodislmodlem  18911  mplcoe1  19446  mplcoe3  19447  mplcoe5  19449  cply1mul  19645  coe1fzgsumdlem  19652  gsummoncoe1  19655  pf1ind  19700  evl1gsumdlem  19701  cnfldmulg  19759  cnfldexp  19760  obslbs  20055  mat1dimcrng  20264  ma1repveval  20358  mulmarep1gsum2  20361  gsummatr01lem3  20444  cramerlem3  20476  decpmatmulsumfsupp  20559  mp2pm2mplem4  20595  pm2mpmhmlem1  20604  fvmptnn04if  20635  cayhamlem1  20652  fctop  20789  mretopd  20877  restopnb  20960  restdis  20963  tgcnp  21038  cncls2  21058  cncls  21059  cnntr  21060  cnsscnp  21064  cmpsub  21184  2ndcsep  21243  1stcelcls  21245  lfinpfin  21308  locfincmp  21310  comppfsc  21316  txcn  21410  txlm  21432  xkohaus  21437  qtopres  21482  haushmphlem  21571  cmphmph  21572  connhmph  21573  reghmph  21577  nrmhmph  21578  ptcmpfi  21597  reghaus  21609  fbssfi  21622  fbun  21625  fbfinnfr  21626  isfildlem  21642  fgcl  21663  cfinfil  21678  supfil  21680  ufinffr  21714  fin1aufil  21717  cnpflf  21786  alexsubALTlem3  21834  alexsubALT  21836  cnextfvval  21850  cnextcn  21852  tmdmulg  21877  tmdgsum  21880  tgphaus  21901  tgpt1  21902  mettri  22138  imasdsf1olem  22159  blssexps  22212  blssex  22213  mopni3  22280  metss  22294  psmetutop  22353  dscmet  22358  tngngp3  22441  rectbntr0  22616  metnrmlem1a  22642  fsumcn  22654  lmmbr  23037  caubl  23087  caublcls  23088  bcthlem5  23106  bcth3  23109  ovolunlem1a  23245  ovoliunnul  23256  ovolicc2lem3  23268  finiunmbl  23293  voliunlem1  23299  volsuplem  23304  volsup  23305  dyadmax  23347  itgfsum  23574  dvnadd  23673  dvnres  23675  cpnord  23679  dvnfre  23696  dvmptfsum  23719  dvlip  23737  fta1g  23908  plyco  23978  dgrcolem1  24010  dgrco  24012  dvnply2  24023  plydivex  24033  plyexmo  24049  aannenlem1  24064  aaliou3lem2  24079  dvntaylp  24106  taylthlem1  24108  ulmval  24115  cxpmul2  24416  scvxcvx  24693  jensenlem2  24695  jensen  24696  ppiub  24910  bcmono  24983  bpos1lem  24988  bposlem5  24994  gausslemma2dlem6  25078  lgsquad2lem2  25091  2lgslem3  25110  2lgs  25113  dchrisumlem1  25159  dchrisum0flb  25180  pntpbnd1  25256  pntlemf  25275  qabvle  25295  qabvexp  25296  ostthlem2  25298  ostth2lem2  25304  axeuclidlem  25823  axcontlem12  25836  umgrnloopv  25982  uhgredgrnv  26006  edglnl  26019  numedglnl  26020  usgruspgrb  26057  usgrnloopvALT  26074  usgredg2vlem2  26099  subupgr  26160  nbumgr  26224  uhgrnbgr0nb  26231  nbgr0vtxlem  26232  edgusgrnbfin  26256  nb3grprlem2  26264  uvtxanbgrvtx  26274  cplgrop  26314  cusgrfi  26335  fusgrmaxsize  26341  fusgrn0degnn0  26376  ewlkprop  26480  uspgr2wlkeq  26523  g0wlk0  26529  wlkreslem  26547  wlkres  26548  lfgriswlk  26566  upgrwlkdvde  26614  spthonepeq  26629  uhgrwkspth  26632  usgr2trlncl  26637  usgr2trlspth  26638  cyclnspth  26676  crctcshwlkn0lem3  26685  wwlksn  26710  wspthneq1eq2  26726  wwlksm1edg  26748  wwlksnred  26768  wwlksnextfun  26774  wwlksnextinj  26775  wwlksnextproplem3  26787  wspthsnonn0vne  26794  rusgrnumwwlk  26851  clwwlksn  26862  clwlkclwwlklem2  26882  clwlkclwwlklem3  26883  umgrclwwlksge2  26892  wwlksubclwwlks  26905  clwwisshclwws  26908  clwwisshclwwsn  26909  clwlksfclwwlk  26942  upgr3v3e3cycl  27020  uhgr3cyclex  27022  upgr4cycl4dv4e  27025  eupthseg  27046  upgreupthseg  27049  eupth2lem3lem4  27071  eupth2lem3lem7  27074  eupth2  27079  eulerpath  27081  nfrgr2v  27116  frgr3vlem1  27117  3vfriswmgr  27122  1to2vfriswmgr  27123  1to3vfriswmgr  27124  3cyclfrgrrn1  27129  3cyclfrgrrn  27130  3cyclfrgrrn2  27131  4cycl2vnunb  27134  frgrncvvdeqlem2  27144  frgrncvvdeqlem8  27150  frgrncvvdeqlem9  27151  frgrwopreglem4  27157  frgrregorufr0  27162  frgr2wwlk1  27167  frgr2wwlkeqm  27169  fusgr2wsp2nb  27172  2wspmdisj  27175  frrusgrord  27179  numclwwlkovf2ex  27191  numclwlk1lem2foa  27195  numclwlk1lem2f1  27198  frgrreggt1  27221  friendshipgt3  27226  hlim2  28019  elnlfn  28757  stle0i  29068  hstrbi  29095  spansncv2  29122  h1da  29178  fmptcof2  29430  nnindd  29540  xreceu  29604  tpr2rico  29932  hasheuni  30121  ismeas  30236  sseqp1  30431  rrvsum  30490  dstfrvunirn  30510  sgn3da  30577  bnj607  30960  bnj1145  31035  bnj1204  31054  subfacp1lem6  31141  cvmliftlem7  31247  cvmliftlem10  31250  cvmlift2lem12  31270  cvmlift3lem4  31278  mrsubvrs  31393  climuzcnv  31539  iprodefisumlem  31601  fprb  31645  dfon2lem9  31670  trpredtr  31704  trpredmintr  31705  dftrpred3g  31707  trpredrec  31712  soseq  31725  frrlem11  31766  sltval2  31783  sltsolem1  31800  linethru  32235  elhf2  32257  finminlem  32287  fnessref  32327  neibastop2lem  32330  fnemeet2  32337  nndivsub  32431  bj-cbval2v  32712  bj-xpnzex  32921  bj-intss  33028  mptsnunlem  33156  dissneqlem  33158  topdifinffinlem  33166  iooelexlt  33181  wl-exeq  33292  wl-ax11-lem3  33335  matunitlindflem1  33376  poimirlem22  33402  poimirlem26  33406  poimirlem28  33408  poimirlem29  33409  poimirlem32  33412  heicant  33415  ovoliunnfl  33422  voliunnfl  33424  volsupnfl  33425  cover2  33479  upixp  33495  sdclem2  33509  fdc  33512  seqpo  33514  metf1o  33522  mettrifi  33524  sstotbnd3  33546  heibor1lem  33579  heiborlem5  33585  heibor  33591  bfplem1  33592  elghomlem2OLD  33656  grpokerinj  33663  isrngo  33667  rngodm1dm2  33702  ispridl2  33808  exlimddvf  33897  lssatle  34121  4atexlemex4  35178  mzpsubst  37130  jm2.18  37374  wepwsolem  37431  iunrelexp0  37813  relexpmulg  37821  cnvtrclfv  37835  clsk1indlem3  38161  dvgrat  38331  radcnvrat  38333  sbcoreleleqVD  38915  csbxpgVD  38950  sineq0ALT  38993  islptre  39651  iblspltprt  39952  stoweidlem2  39982  stoweidlem17  39997  stoweidlem21  40001  2reu2  40950  afveu  40996  funbrafv  41001  ndmaovass  41049  funop1  41065  nltle2tri  41086  2elfz2melfz  41091  fzoopth  41100  smonoord  41105  fsummsndifre  41106  fsumsplitsndif  41107  fsummmodsndifre  41108  fsummmodsnunz  41109  iccpartimp  41117  iccpartiltu  41122  iccpartigtl  41123  iccpartleu  41128  iccpartgel  41129  iccpartrn  41130  iccpartiun  41134  icceuelpart  41136  iccpartnel  41138  fargshiftf  41140  fargshiftf1  41141  pfxccatin12lem2  41189  pfxccat3  41191  fmtnoinf  41213  odz2prm2pw  41240  lighneallem4  41292  lighneal  41293  evensumeven  41381  even3prm2  41393  gbowgt5  41415  nnsum4primeseven  41453  nnsum4primesevenALTV  41454  bgoldbnnsum3prm  41457  bgoldbtbndlem2  41459  bgoldbtbndlem4  41461  bgoldbtbnd  41462  elsprel  41490  prsprel  41502  sprsymrelfo  41512  clcllaw  41592  nrhmzr  41638  rnghmmul  41665  rngccatidALTV  41754  ringccatidALTV  41817  nzerooringczr  41837  scmsuppss  41918  gsumlsscl  41929  ply1mulgsumlem2  41940  lincvalsc0  41975  linc0scn0  41977  lincdifsn  41978  linc1  41979  lincellss  41980  lincsum  41983  lincscm  41984  lincsumcl  41985  lcoss  41990  lincext3  42010  lindslinindimp2lem4  42015  lindslinindsimp2lem5  42016  lindslinindsimp2  42017  lindsrng01  42022  snlindsntor  42025  lincresunit3lem2  42034  lincresunit3  42035  islindeps2  42037  blengt1fldiv2p1  42152
  Copyright terms: Public domain W3C validator