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

Theorem expcom 449
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 448 . 2 (𝜑 → (𝜓𝜒))
32com12 32 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  ancoms  467  syldan  485  sylan  486  4casesdan  987  dedlema  992  dedlemb  993  19.40bOLD  1804  cbval2  2262  cbvaldva  2264  2moswap  2531  2eu2  2538  pm2.61ne  2863  nelelne  2876  r19.21be  2913  minel  3981  uneqdifeq  4005  uneqdifeqOLD  4006  raltpd  4254  ssunsn2  4293  ssuni  4386  ssuniOLD  4387  uniss2  4397  elpwuni  4540  elssabg  4738  elpw2g  4746  oteqex  4880  otsndisj  4892  otiunsndisj  4893  epelg  4937  wereu  5021  relop  5179  riinint  5287  sotri3  5429  unixpid  5570  ordtr2  5668  ordsssuc2  5714  funopg  5819  fun  5962  tz6.12c  6105  fvmptnf  6192  fvn0ssdmfun  6240  eldmrexrnb  6256  fmptco  6285  fnressn  6305  fressnfv  6307  fvtp2g  6344  fvtp3g  6345  fconst2g  6348  fntpb  6353  f1dom3el3dif  6401  isores3  6460  isoselem  6466  oprabv  6576  eloprabga  6620  sorpsscmpl  6820  difex2  6837  ordpwsuc  6881  ordsucun  6891  limuni3  6918  ordom  6940  fo1stres  7057  poxp  7150  soxp  7151  suppimacnv  7167  frnsuppeq  7168  funsssuppss  7182  brtpos2  7219  wfrlem12  7287  onnseq  7302  smores  7310  smofvon2  7314  tfrlem1  7333  oacl  7476  omcl  7477  oecl  7478  oawordri  7491  oalimcl  7501  oaass  7502  oarec  7503  omwordri  7513  omeulem1  7523  omeulem2  7524  oeordi  7528  oeworde  7534  oeoelem  7539  nnacl  7552  nnmcl  7553  nnecl  7554  nnacom  7558  nnaass  7563  nnmsucr  7566  nnmordi  7572  omabs  7588  iiner  7680  elpmg  7733  pmss12g  7744  mapsn  7759  f1domg  7835  ssdomg  7861  domtriord  7965  php  8003  php3  8005  1sdom  8022  fisseneq  8030  isinf  8032  ssnnfi  8038  dif1en  8052  findcard3  8062  frfi  8064  unfi  8086  difinf  8089  fnfi  8097  iunfi  8111  fsuppunfi  8152  fsuppres  8157  frnfsuppbi  8161  elfi2  8177  marypha1lem  8196  marypha1  8197  oiexg  8297  wemapso2  8315  harword  8327  brwdom  8329  unxpwdom  8351  en3lplem1  8368  inf3lemd  8381  inf3lem5  8386  cantnfval2  8423  cantnfle  8425  cantnflt  8426  cnfcom  8454  tcmin  8474  r1sdom  8494  rankxplim3  8601  cardidm  8642  cardmin2  8681  infxpenlem  8693  fseqenlem1  8704  numacn  8729  alephordi  8754  iscard3  8773  alephinit  8775  carduniima  8776  iunfictbso  8794  dfac5  8808  dfac12lem3  8824  pwsdompw  8883  pwcdadom  8895  cflim2  8942  cfslb2n  8947  cofsmo  8948  cfsmolem  8949  cfcoflem  8951  alephsing  8955  infpssALT  8992  fin23lem34  9025  isf32lem2  9033  isf32lem10  9041  isf32lem12  9043  isfin1-2  9064  hsmexlem4  9108  axcc2lem  9115  domtriomlem  9121  axdc2lem  9127  axdc3lem2  9130  axdc3lem4  9132  axdc4lem  9134  axcclem  9136  ac6num  9158  ac6s  9163  zorn2lem7  9181  ttukeylem5  9192  imadomg  9211  iundom2g  9215  ondomon  9238  ficard  9240  konigthlem  9243  alephreg  9257  pwcfsdom  9258  cfpwsdom  9259  axregndlem1  9277  axregnd  9279  pwfseqlem3  9335  pwxpndom2  9340  pwxpndom  9341  pwcdandom  9342  inawinalem  9364  gchina  9374  wuncval2  9422  tsk0  9438  tskxpss  9447  inatsk  9453  tskuni  9458  gruina  9493  grothac  9505  addclpi  9567  addnidpi  9576  nqereu  9604  mulcanenq  9635  genpnnp  9680  nqpr  9689  prlem934  9708  reclem2pr  9723  suplem1pr  9727  supsrlem  9785  axpre-sup  9843  1re  9892  dedekindle  10049  00id  10059  receu  10518  sup3  10826  infrelb  10852  peano5nni  10867  nnaddcl  10886  zrevaddcl  11252  nzadd  11255  zdiv  11276  nneo  11290  zeo2  11293  nn0indd  11303  fzind  11304  fnn0ind  11305  uzwo  11580  lbzbi  11605  nn01to3  11610  qrevaddcl  11639  irradd  11641  irrmul  11642  ltsubrp  11695  ltaddrp  11696  icoshft  12118  fzen  12181  elfzm11  12232  uzsplit  12233  elfzoext  12344  elfzom1elp1fzo  12354  injresinjlem  12402  injresinj  12403  modifeq2int  12546  modsumfzodifsn  12557  om2uzlti  12563  ssnn0fi  12598  fsuppmapnn0fiub0  12607  mptnn0fsuppr  12613  seqcl2  12633  seqfveq2  12637  seqshft2  12641  monoord  12645  seqsplit  12648  seqcaopr3  12650  seqf1olem2a  12653  seqf1o  12656  seqid2  12661  seqhomo  12662  ser1const  12671  expadd  12716  expmul  12719  leexp1a  12733  faccl  12884  facdiv  12888  faclbnd  12891  faclbnd4lem4  12897  faclbnd6  12900  hasheqf1oi  12951  hasheqf1oiOLD  12952  hashf1rnOLD  12954  hashgadd  12976  hashinfxadd  12984  hashunx  12985  hashunsng  12991  elprchashprn2  12994  hashle00  12998  hashss  13007  hash1snb  13017  hashmap  13031  hashf1lem2  13046  hashf1  13047  seqcoll  13054  hashge2el2dif  13064  hashge3el3dif  13069  hash1to3  13075  fi1uzind  13077  brfi1indALT  13080  fi1uzindOLD  13083  brfi1indALTOLD  13086  sswrd  13111  swrdnd2  13228  swrdswrdlem  13254  swrdswrd  13255  wrd2ind  13272  swrdccatin1  13277  swrdccatin2  13281  swrdccatin12lem2  13283  swrdccat3  13286  repsdf2  13319  repswswrd  13325  cshw0  13334  cshwcl  13338  cshwlen  13339  cshf1  13350  swrdco  13377  relexpsucnnl  13563  rtrclreclem3  13591  rtrclreclem4  13592  relexpindlem  13594  rtrclind  13596  shftlem  13599  caubnd  13889  rlimcld2  14100  o1dif  14151  climub  14183  climserle  14184  iseraltlem2  14204  sumss  14245  fsumzcl2  14259  fsummsnunz  14270  fsumsplitsnun  14271  fsum2d  14287  modfsummods  14309  fsumabs  14317  fsumrlim  14327  fsumo1  14328  fsumiun  14337  bcxmas  14349  climcndslem1  14363  climcndslem2  14364  cvgrat  14397  clim2prod  14402  prodfn0  14408  prodfrec  14409  ntrivcvg  14411  prodmo  14448  fprodss  14460  fprodabs  14486  fprodn0  14491  fprod2d  14493  fprodefsum  14607  ruclem8  14748  ruclem9  14749  dvds2ln  14795  dvdsaddre2b  14810  dvdslelem  14812  dvdsdivcl  14819  alzdvds  14823  mod2eq1n2dvds  14852  oddnn02np1  14853  nn0o1gt2  14878  nno  14879  sumeven  14891  sumodd  14892  pwp1fsum  14895  ndvdsadd  14915  bitsinv1  14945  sadcadd  14961  sadadd2  14963  saddisjlem  14967  smuval2  14985  smupvallem  14986  smu01lem  14988  smupval  14991  smueqlem  14993  smumullem  14995  gcddiv  15049  gcdmultiple  15050  rplpwr  15057  nn0seqcvgd  15064  seq1st  15065  alginv  15069  algcvga  15073  algfx  15074  absprodnn  15112  isprm2  15176  isprm3  15177  prmind2  15179  maxprmfct  15202  prmdvdsexp  15208  pcmpt  15377  prmreclem4  15404  vdwmc2  15464  vdwlem10  15475  ramub2  15499  ramcl  15514  prmgaplem5  15540  prmgaplem8  15543  cshwshashlem1  15583  cshwshashlem3  15585  imasleval  15967  divsfval  15973  mreexexlem4d  16073  isssc  16246  initoeu1  16427  termoeu1  16434  istos  16801  mgmcl  17011  frmdgsum  17165  dfgrp3lem  17279  mhmmulg  17349  resghm2b  17444  gsumwrev  17562  elsymgbas  17568  symgextf1  17607  gsmsymgreqlem2  17617  gsmsymgreq  17618  odlem1  17720  odcl2  17748  gexlem1  17760  sylow1lem1  17779  efgi2  17904  efginvrel2  17906  efgsrel  17913  cyggexb  18066  gsummulglem  18107  gsumzunsnd  18121  gsum2dlem2  18136  telgsums  18156  dmdprd  18163  dprdw  18175  ablfac1eulem  18237  srgpcomp  18298  lmodfopnelem1  18665  mplcoe1  19229  mplcoe3  19230  mplcoe5  19232  cply1mul  19428  coe1fzgsumdlem  19435  gsummoncoe1  19438  pf1ind  19483  evl1gsumdlem  19484  cnfldmulg  19540  cnfldexp  19541  obslbs  19832  mat1dimcrng  20041  ma1repveval  20135  mulmarep1gsum2  20138  gsummatr01lem3  20221  cramerlem3  20253  decpmatmulsumfsupp  20336  mp2pm2mplem4  20372  pm2mpmhmlem1  20381  fvmptnn04if  20412  cayhamlem1  20429  fctop  20557  mretopd  20645  restopnb  20728  restdis  20731  tgcnp  20806  cncls2  20826  cncls  20827  cnntr  20828  cnsscnp  20832  cmpsub  20952  2ndcsep  21011  1stcelcls  21013  lfinpfin  21076  locfincmp  21078  comppfsc  21084  txcn  21178  txlm  21200  xkohaus  21205  qtopres  21250  haushmphlem  21339  cmphmph  21340  conhmph  21341  reghmph  21345  nrmhmph  21346  ptcmpfi  21365  reghaus  21377  fbssfi  21390  fbun  21393  fbfinnfr  21394  isfildlem  21410  fgcl  21431  cfinfil  21446  supfil  21448  ufinffr  21482  fin1aufil  21485  cnpflf  21554  alexsubALTlem3  21602  alexsubALT  21604  cnextfvval  21618  cnextcn  21620  tmdmulg  21645  tmdgsum  21648  tgphaus  21669  tgpt1  21670  mettri  21905  imasdsf1olem  21926  blssexps  21979  blssex  21980  mopni3  22047  metss  22061  psmetutop  22120  dscmet  22125  rectbntr0  22372  metnrmlem1a  22397  fsumcn  22409  lmmbr  22779  caubl  22828  caublcls  22829  bcthlem5  22847  bcth3  22850  ovolunlem1a  22985  ovoliunnul  22996  ovolicc2lem3  23008  finiunmbl  23033  voliunlem1  23039  volsuplem  23044  volsup  23045  dyadmax  23086  itgfsum  23313  dvnadd  23412  dvnres  23414  cpnord  23418  dvnfre  23435  dvmptfsum  23456  dvlip  23474  fta1g  23645  plyco  23715  dgrcolem1  23747  dgrco  23749  dvnply2  23760  plydivex  23770  plyexmo  23786  aannenlem1  23801  aaliou3lem2  23816  dvntaylp  23843  taylthlem1  23845  ulmval  23852  cxpmul2  24149  scvxcvx  24426  jensenlem2  24428  jensen  24429  ppiub  24643  bcmono  24716  bpos1lem  24721  bposlem5  24727  gausslemma2dlem6  24811  lgsquad2lem2  24824  2lgslem3  24843  2lgs  24846  dchrisumlem1  24892  dchrisum0flb  24913  pntpbnd1  24989  pntlemf  25008  qabvle  25028  qabvexp  25029  ostthlem2  25031  ostth2lem2  25037  axeuclidlem  25557  axcontlem12  25570  usgraedgprv  25668  usgranloopv  25670  usgraidx2vlem2  25684  usgrafisbase  25706  edgusgranbfin  25742  nb3graprlem2  25744  cusgra2v  25754  cusgrafi  25773  sizeusglecusglem1  25775  sizeusglecusg  25777  usgramaxsize  25778  iswlkg  25815  2trllemH  25845  2trllemE  25846  usgrwlknloop  25856  spthonepeq  25880  wlkdvspthlem  25900  wlkdvspth  25901  usgra2wlkspthlem1  25910  usgra2wlkspthlem2  25911  cyclnspth  25922  fargshiftf  25927  fargshiftf1  25928  3v3e3cycl2  25955  3v3e3cycl  25956  4cycl4dv  25958  wwlkn0  25980  usg2wlkeq  25999  wwlknred  26014  wwlkextfun  26020  wwlkextinj  26021  wwlkm1edg  26026  wwlkextproplem3  26034  clwwlkgt0  26062  clwlkisclwwlklem1  26078  clwlkisclwwlklem0  26079  wwlksubclwwlk  26095  clwwisshclww  26098  clwwisshclwwn  26099  clwlkfclwwlk  26134  2wlkonot3v  26165  2spthonot3v  26166  usg2wlkonot  26173  usg2wotspth  26174  usgfidegfi  26200  cusgraisrusgra  26228  rusgranumwlk  26247  iseupa  26255  eupatrl  26258  eupath2  26270  frgra2v  26289  frgra3vlem1  26290  3vfriswmgra  26295  1to2vfriswmgra  26296  1to3vfriswmgra  26297  2pthfrgra  26301  3cyclfrgrarn1  26302  3cyclfrgrarn  26303  3cyclfrgrarn2  26304  4cycl2vnunb  26307  vdn0frgrav2  26313  vdgn0frgrav2  26314  frgrancvvdeqlem4  26323  frgrancvvdeqlemB  26328  frgrancvvdeqlemC  26329  frgrawopreglem2  26335  frgrawopreglem4  26337  frgrawopreg  26339  frgraregorufr0  26342  frgraeu  26344  frg2woteqm  26349  2spotmdisj  26358  usgreghash2spot  26359  clwwlkextfrlem1  26366  numclwwlkovf2ex  26376  numclwlk1lem2foa  26381  numclwlk1lem2f1  26384  frgrareg  26407  friendshipgt3  26411  hlim2  27236  elnlfn  27974  stle0i  28285  hstrbi  28312  spansncv2  28339  h1da  28395  fmptcof2  28642  nnindd  28756  xreceu  28764  tpr2rico  29089  hasheuni  29277  ismeas  29392  sseqp1  29587  rrvsum  29646  dstfrvunirn  29666  sgn3da  29733  bnj607  30043  bnj1145  30118  bnj1204  30137  subfacp1lem6  30224  cvmliftlem7  30330  cvmliftlem10  30333  cvmlift2lem12  30353  cvmlift3lem4  30361  mrsubvrs  30476  climuzcnv  30622  iprodefisumlem  30682  fprb  30719  dfon2lem9  30743  trpredtr  30777  trpredmintr  30778  dftrpred3g  30780  trpredrec  30785  soseq  30798  frrlem11  30839  sltval2  30856  sltsolem1  30870  linethru  31233  elhf2  31255  finminlem  31285  fnessref  31325  neibastop2lem  31328  fnemeet2  31335  nndivsub  31429  bj-cbval2v  31727  bj-xpnzex  31939  mptsnunlem  32161  dissneqlem  32163  topdifinffinlem  32171  iooelexlt  32186  wl-exeq  32300  wl-ax11-lem3  32343  matunitlindflem1  32375  poimirlem22  32401  poimirlem26  32405  poimirlem28  32407  poimirlem29  32408  poimirlem32  32411  heicant  32414  ovoliunnfl  32421  voliunnfl  32423  volsupnfl  32424  cover2  32478  upixp  32494  sdclem2  32508  fdc  32511  seqpo  32513  metf1o  32521  mettrifi  32523  sstotbnd3  32545  heibor1lem  32578  heiborlem5  32584  heibor  32590  bfplem1  32591  elghomlem2OLD  32655  grpokerinj  32662  isrngo  32666  rngodm1dm2  32701  ispridl2  32807  exlimddvf  32896  lssatle  33120  4atexlemex4  34177  mzpsubst  36129  jm2.18  36373  wepwsolem  36430  iunrelexp0  36813  relexpmulg  36821  cnvtrclfv  36835  clsk1indlem3  37161  dvgrat  37333  radcnvrat  37335  sbcoreleleqVD  37917  csbxpgVD  37952  sineq0ALT  37995  islptre  38487  iblspltprt  38666  stoweidlem2  38696  stoweidlem17  38711  stoweidlem21  38715  2reu2  39637  afveu  39684  funbrafv  39689  ndmaovass  39737  nltle2tri  39744  smonoord  39746  iccpartimp  39757  iccpartiltu  39762  iccpartigtl  39763  iccpartleu  39768  iccpartgel  39769  iccpartrn  39770  iccpartiun  39774  icceuelpart  39776  iccpartnel  39778  fmtnoinf  39788  odz2prm2pw  39815  lighneallem4  39867  lighneal  39868  evensumeven  39956  gbogt5  39986  nnsum4primeseven  40018  nnsum4primesevenALTV  40019  bgoldbnnsum3prm  40022  bgoldbtbndlem2  40024  bgoldbtbndlem4  40026  bgoldbtbnd  40027  pfxccatin12lem2  40089  pfxccat3  40091  funopsn  40141  funop1  40143  fundmge2nop0  40149  2elfz2melfz  40179  fzoopth  40184  xnn0xaddcl  40212  xnn0xadd0  40214  fsummsndifre  40218  fsumsplitsndif  40219  fsummmodsndifre  40220  fsummmodsnunz  40221  uhgrstrrepelem  40302  umgrnloopv  40330  uhgredgrnv  40362  usgruspgrb  40410  usgrnloopvALT  40427  usgredg2vlem2  40452  subupgr  40510  nbumgr  40568  uhgrnbgr0nb  40575  nbgr0vtxlem  40576  edgusgrnbfin  40600  nb3grprlem2  40608  uvtxanbgrvtx  40618  cplgrop  40658  cusgrfi  40673  fusgrmaxsize  40679  fusgrn0degnn0  40713  ewlkprop  40804  upgrwlkedg  40849  uspgr2wlkeq  40853  g01wlk0  40859  1wlkreslem  40877  1wlkres  40878  lfgriswlk  40896  upgrwlkdvde  40942  spthonepeq-av  40957  uhgr1wlkspth  40960  usgr2trlncl  40965  usgr2trlspth  40966  cyclnsPth  41005  crctcsh1wlkn0lem3  41014  wwlksn  41039  wspthneq1eq2  41055  wwlksm1edg  41077  wwlksnred  41097  wwlksnextfun  41103  wwlksnextinj  41104  wwlksnextproplem3  41116  wspthsnonn0vne  41123  rusgrnumwwlk  41177  clwwlksn  41188  clwlkclwwlklem2  41208  clwlkclwwlklem3  41209  umgrclwwlksge2  41218  wwlksubclwwlks  41231  clwwisshclwws  41234  clwwisshclwwsn  41235  clwlksfclwwlk  41268  upgr3v3e3cycl  41346  uhgr3cyclex  41348  upgr4cycl4dv4e  41351  eupthseg  41373  upgreupthi  41375  upgreupthseg  41376  eupth2lem3lem4  41398  eupth2lem3lem7  41401  eupth2  41406  eulerpath  41408  nfrgr2v  41441  frgr3vlem1  41442  3vfriswmgr  41447  1to2vfriswmgr  41448  1to3vfriswmgr  41449  3cyclfrgrrn1  41454  3cyclfrgrrn  41455  3cyclfrgrrn2  41456  4cycl2vnunb-av  41459  frgrncvvdeqlem4  41471  frgrncvvdeqlemB  41476  frgrncvvdeqlemC  41477  frgrwopreglem4  41483  frgrwopreg  41485  frgrregorufr0  41488  frgreu  41490  frgr2wwlk1  41493  fusgr2wsp2nb  41497  2wspmdisj  41500  fusgreghash2wsp  41501  av-numclwwlkovf2ex  41516  av-numclwlk1lem2foa  41520  av-numclwlk1lem2f1  41523  av-frgrareggt1  41546  av-friendshipgt3  41551  clcllaw  41616  nrhmzr  41662  rnghmmul  41689  rngccatidALTV  41780  ringccatidALTV  41843  nzerooringczr  41863  scmsuppss  41946  gsumlsscl  41957  ply1mulgsumlem2  41968  lincvalsc0  42003  linc0scn0  42005  lincdifsn  42006  linc1  42007  lincellss  42008  lincsum  42011  lincscm  42012  lincsumcl  42013  lcoss  42018  lincext3  42038  lindslinindimp2lem4  42043  lindslinindsimp2lem5  42044  lindslinindsimp2  42045  lindsrng01  42050  snlindsntor  42053  lincresunit3lem2  42062  lincresunit3  42063  islindeps2  42065  blengt1fldiv2p1  42184
  Copyright terms: Public domain W3C validator