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

Theorem ancoms 468
Description: Inference commuting conjunction in antecedent. (Contributed by NM, 21-Apr-1994.)
Hypothesis
Ref Expression
ancoms.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
ancoms ((𝜓𝜑) → 𝜒)

Proof of Theorem ancoms
StepHypRef Expression
1 ancoms.1 . . 3 ((𝜑𝜓) → 𝜒)
21expcom 450 . 2 (𝜓 → (𝜑𝜒))
32imp 444 1 ((𝜓𝜑) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 385
This theorem is referenced by:  adantl  473  syl2anr  496  anim12ci  592  sylan9bbr  739  anabss4  891  anabsi7  895  anabsi8  896  im2anan9r  917  bi2anan9r  954  syl3anr2  1526  mp3anr1  1566  mp3anr2  1567  mp3anr3  1568  stoic1b  1843  dvelimf  2470  2eu3  2689  eqeqan12rd  2774  sylan9eqr  2812  r19.29vva  3215  morex  3527  sbcrext  3648  sbcrextOLD  3649  sylan9ssr  3754  pssdifcom1  4194  pssdifcom2  4195  preq12nebg  4539  opthprneg  4541  riinn0  4743  breqan12rd  4817  propeqop  5114  soinxp  5336  frinxp  5337  seinxp  5338  brelrng  5506  dminss  5701  imainss  5702  sossfld  5734  cnvsng  5771  setlikespec  5858  ordelssne  5907  ordtri3or  5912  ordtri2  5915  ordtri4  5918  ordtr3OLD  5927  ordtri2or  5979  funsng  6094  f1co  6267  f1ocnv  6306  f1oprswap  6337  funimass4  6405  dffv2  6429  fndmdifcom  6481  fsn2  6562  fvtp2  6621  fvtp3  6622  fvtp2g  6624  fvtp3g  6625  soisoi  6737  riotaeqimp  6793  oveqan12rd  6829  brrpssg  7100  sorpsscmpl  7109  dfwe2  7142  ordsucelsuc  7183  ordunisuc2  7205  tfindsg  7221  tfindsg2  7222  dfom2  7228  funcnvuni  7280  fun11iun  7287  cofunex2g  7292  curry2  7436  soxp  7454  mpt2xopoveqd  7512  tposoprab  7553  wfr3g  7578  wfrlem5  7584  wfrlem10  7589  smores3  7615  smores2  7616  smoel  7622  dfrecs3  7634  tfr3  7660  tz7.48-2  7702  tz7.49  7705  oaordi  7791  oaword  7794  oaord1  7796  oaword2  7798  oa00  7804  oalimcl  7805  oaass  7806  oarec  7807  oacomf1o  7810  omord2  7812  omcan  7814  omword  7815  omword1  7818  omword2  7819  odi  7824  omass  7825  oneo  7826  oen0  7831  oecan  7834  oelim2  7840  nnarcl  7861  nnaordi  7863  nnaordr  7865  nnawordi  7866  nnmsucr  7870  nnmcom  7871  nnaword  7872  nnmordi  7876  nnaordex  7883  oaabslem  7888  omabslem  7891  nnneo  7896  omsmo  7899  ersym  7919  elecg  7948  riiner  7983  ecopovsym  8012  ecovcom  8016  mapvalg  8029  pmvalg  8030  elpmg  8035  elmapssres  8044  pmss12g  8046  ixpconstg  8079  ener  8164  domtr  8170  f1imaeng  8177  fundmen  8191  xpcomco  8211  xpsnen2g  8214  xpdom2  8216  xpdom1g  8218  omxpen  8223  omf1o  8224  enen2  8262  domen2  8264  sdomen2  8266  domtriord  8267  sdomel  8268  onsdominel  8270  infensuc  8299  onomeneq  8311  nndomo  8315  pssnn  8339  unbnn  8377  infcntss  8395  fiint  8398  mapfi  8423  fiin  8489  fiss  8491  infempty  8573  oiiso  8603  unwdomg  8650  suc11reg  8685  inf3lem5  8698  infeq5  8703  cantnfp1lem3  8746  r1tr  8808  r1val1  8818  rankr1ai  8830  rankonidlem  8860  onssr1  8863  tskwe  8962  carddom2  8989  carden2  8999  domtri2  9001  cardval2  9003  fidomtri  9005  fidomtri2  9006  harval2  9009  dif1card  9019  infxpenlem  9022  ac5num  9045  alephord3  9087  alephdom  9090  aleph11  9093  alephdom2  9096  cardaleph  9098  dfac3  9130  dfac5  9137  cdacomen  9191  onacda  9207  pwsdompw  9214  ackbij1lem11  9240  ackbij2  9253  cfeq0  9266  cfsuc  9267  cff1  9268  cflim2  9273  cfsmolem  9280  coftr  9283  sornom  9287  infpssrlem4  9316  ssfin4  9320  ssfin2  9330  ssfin3ds  9340  fin23lem31  9353  isf32lem9  9371  hsmexlem5  9440  axdc3lem  9460  axdc3lem2  9461  axdc3lem4  9463  zorn2lem6  9511  brdom3  9538  brdom7disj  9541  brdom6disj  9542  alephval2  9582  alephreg  9592  wuncss  9755  gruen  9822  addcompi  9904  mulcompi  9906  ltapi  9913  ltmpi  9914  nqereu  9939  addcompq  9960  addcomnq  9961  mulcompq  9962  mulcomnq  9963  ltsonq  9979  ltanq  9981  ltmnq  9982  genpnnp  10015  addcompr  10031  mulcompr  10033  ltsopr  10042  ltexprlem2  10047  prlem936  10057  suplem2pr  10063  map2psrpr  10119  axpre-ltadd  10176  xrltnle  10293  axlttri  10297  axsup  10301  ltnle  10305  letri3  10311  leloe  10312  eqlelt  10313  letric  10325  mul31  10392  subcl  10468  pncan2  10476  pncan3  10477  npcan  10478  addsubeq4  10484  npncan3  10507  negsubdi2  10528  muladd  10650  subdi  10651  mulneg2  10655  mulsub  10661  ltleadd  10699  ltsubpos  10708  posdif  10709  addge01  10726  lesub0  10733  wloglei  10748  prodgt02  11057  prodge02  11059  mulsuble0b  11083  ltdivmul  11086  ledivmul  11087  lt2mul2div  11089  lerec  11094  lt2msq  11096  ltdiv23  11102  lediv23  11103  lediv2a  11105  le2msq  11111  msq11  11112  fimaxre  11156  lbreu  11161  infm3  11170  dfinfre  11192  creur  11202  creui  11203  cju  11204  nnmulcl  11231  nndivtr  11250  avgle1  11460  avgle2  11461  avgle  11462  nn0nnaddcl  11512  ltsubnn0  11532  zrevaddcl  11610  znnsub  11611  znn0sub  11612  zextlt  11639  gtndiv  11642  prime  11646  uztrn2  11893  uztric  11897  uz11  11898  nn0pzuz  11934  uzwo  11940  zmax  11974  zbtwnre  11975  rebtwnz  11976  qrevaddcl  11999  rpnnen1lem2  12003  rpnnen1lem1  12004  rpnnen1lem3  12005  rpnnen1lem5  12007  rpnnen1lem1OLD  12010  rpnnen1lem3OLD  12011  rpnnen1lem5OLD  12013  difrp  12057  xrltnsym  12159  xrlttri  12161  xrleloe  12166  xrletri  12173  xrletri3  12174  xrmaxeq  12199  xrmineq  12200  xrmaxlt  12201  xrmaxle  12203  lemaxle  12215  z2ge  12218  qbtwnre  12219  qextlt  12223  qextle  12224  xleneg  12238  xaddcom  12260  xmulcom  12285  xmulneg2  12289  xmulgt0  12302  xrsupsslem  12326  xrinfmsslem  12327  supxrunb1  12338  supxrunb2  12339  ixxssixx  12378  ixxin  12381  ioon0  12390  iccid  12409  iooshf  12441  iccsupr  12455  iooneg  12481  iccneg  12482  iccsplit  12494  fzen  12547  fzadd2  12565  fzass4  12568  fzrev  12592  fznn  12597  elfzp1b  12606  elfzm1b  12607  fz0fzdiffz0  12638  difelfznle  12643  fzon  12679  fzo0n  12680  fzonmapblen  12704  elfzoext  12715  eluzgtdifelfzo  12720  ubmelm1fzo  12754  elfzom1elp1fzo1  12758  subfzo0  12780  fllt  12797  flflp1  12798  flbi  12807  flbi2  12808  flzadd  12817  ltdifltdiv  12825  dfceil2  12830  modcyc2  12896  modifeq2int  12922  modaddmodup  12923  modaddmodlo  12924  modfzo0difsn  12932  modsumfzodifsn  12933  om2uzlt2i  12940  om2uzf1oi  12942  fseqsupubi  12967  fsuppmapnn0fiub0  12983  expcllem  13061  mulbinom2  13174  faclbnd5  13275  hashbnd  13313  hasheni  13326  hasheqf1oi  13330  hashdom  13356  hashss  13385  hashfacen  13426  ccatsymb  13550  ccatass  13556  ccatalpha  13561  wrd2ind  13673  swrdccatin12lem2b  13682  swrdccatin2  13683  swrdccatin12lem2  13685  swrdccatin12  13687  swrdccat3blem  13691  swrdccatid  13693  repswsymball  13722  repswsymballbi  13723  cshwsublen  13738  cshwn  13739  cshwlen  13741  cshwidxmod  13745  cshf1  13752  repswcshw  13754  cshweqdif2  13761  cshweqrep  13763  cshwcsh2id  13770  ccatco  13777  swrdco  13779  lswco  13780  s3iunsndisj  13904  relexprelg  13973  relexpnndm  13976  relexpaddnn  13986  shftlem  14003  shftuz  14004  shftfval  14005  shftval4  14012  shftval5  14013  2shfti  14015  seqshft  14020  mulre  14056  sqrtlt  14197  abs3dif  14266  abs2difabs  14269  uzin2  14279  rexanre  14281  caubnd  14293  climshftlem  14500  rlimcn2  14516  fsumcnv  14699  modfsummods  14720  geo2lim  14801  ntrivcvgfvn0  14826  prodmo  14861  zprod  14862  prodss  14872  fprodcnv  14908  bpolysum  14979  bpoly4  14985  efle  15043  reef11  15044  demoivre  15125  demoivreALT  15126  znnenlem  15135  sqrt2irr  15174  nndivides  15188  0dvds  15200  muldvds1  15204  muldvds2  15205  dvdscmulr  15208  dvdssubr  15225  dvdsadd2b  15226  odd2np1  15263  mulsucdiv2z  15275  ltoddhalfle  15283  divalglem9  15322  ndvdssub  15331  gcdcllem1  15419  gcdcom  15433  neggcd  15442  gcdabs2  15450  modgcd  15451  lcmcom  15504  neglcm  15515  lcmgcdeq  15523  coprmdvds  15564  coprmdvdsOLD  15565  qredeq  15569  divgcdcoprmex  15578  dvdsprm  15613  cncongrprm  15635  odzdvds  15698  powm2modprm  15706  modprmn0modprm0  15710  coprimeprodsq  15711  pythagtriplem1  15719  pythagtriplem4  15722  pc2dvds  15781  pc11  15782  pcz  15783  pcprod  15797  prmunb  15816  1arithlem3  15827  1arith  15829  cshwshashlem2  16001  cshwshashlem3  16002  ressabs  16137  acsfn2  16521  issect  16610  funcestrcsetclem9  16985  funcsetcestrclem5  16996  funcsetcestrclem9  17000  pospo  17170  latjcom  17256  latmcom  17272  clatglbss  17324  pospropd  17331  pslem  17403  tsrss  17420  issubmnd  17515  submcl  17550  resmhm2b  17558  frmdmnd  17593  frmd0  17594  grpinvsub  17694  dfgrp3lem  17710  gimcnv  17906  gimco  17907  gictr  17914  cntz2ss  17961  cntzrec  17962  symg2bas  18014  symgextf1  18037  symgfixelsi  18051  pmtrfinv  18077  pmtrdifwrdel2  18102  dfod2  18177  lsmcom2  18266  efgred  18357  qusabl  18464  cygabl  18488  gsummptnn0fz  18578  eldprd  18599  srgmulgass  18727  dfrhm2  18915  isrim0  18921  rmodislmodlem  19128  rmodislmod  19129  lmimcnv  19265  mplcoe5lem  19665  psrbagfsupp  19707  cnfldexp  19977  cnsrng  19978  xrsdsreval  19989  dvdsrzring  20029  znf1o  20098  ocvocv  20213  ocvin  20216  frlmip  20315  islindf  20349  lindff  20352  lindfrn  20358  f1lindf  20359  mamudir  20408  matsca2  20424  matbas2  20425  matlmod  20433  matinvgcell  20439  mat1bas  20453  dmatmul  20501  dmatsgrp  20503  dmatsrng  20505  dmatcrng  20506  scmatsgrp1  20526  scmatsrng1  20527  madulid  20649  gsummatr01lem3  20661  gsummatr01  20663  cpmatacl  20719  0mat2pmat  20739  idmatidpmat  20740  m2cpminv0  20764  pmatcollpw3fi1lem1  20789  chfacfscmulgsum  20863  chfacfpmmulgsum  20867  eltg  20959  eltg2  20960  tgss  20970  tgss2  20989  basgen2  20991  bastop1  20995  cldmre  21080  toponmre  21095  opnneiss  21120  restcldr  21176  restfpw  21181  restcls  21183  restntr  21184  ordtbaslem  21190  ordtrest2lem  21205  leordtvallem2  21213  leordtval  21215  cnrest  21287  t0sep  21326  cmpcov  21390  cmpsublem  21400  cmpsub  21401  bwth  21411  2ndcomap  21459  locfincmp  21527  ptval  21571  xkoval  21588  txss12  21606  ptrescn  21640  xkopt  21656  hmeofval  21759  txswaphmeolem  21805  txswaphmeo  21806  trfbas2  21844  trfbas  21845  uzrest  21898  numufl  21916  ssufl  21919  flimclsi  21979  hauspwpwf1  21988  ghmcnp  22115  blpnfctr  22438  metequiv  22511  metcnp3  22542  elbl4  22565  restmetu  22572  tngngp  22655  qtopbaslem  22759  bl2ioo  22792  ioo2bl  22793  ioo2blex  22794  xrsxmet  22809  divccn  22873  divccncf  22906  isclmi0  23094  iscvsi  23125  causs  23292  lmclim  23297  bcthlem1  23317  ovolfsf  23436  ioombl  23529  iccvolcl  23531  ioovolcl  23534  ioorcl  23541  volcn  23570  itg2itg1  23698  dvexp  23911  dvmptfsum  23933  dvexp3  23936  dvef  23938  dvlip  23951  c1lip1  23955  ftc1a  23995  tdeglem1  24013  tdeglem3  24014  tdeglem4  24015  coe1termlem  24209  plyremlem  24254  ptolemy  24443  cos11  24474  logeftb  24525  logleb  24544  logdivlt  24562  logdivle  24563  angval  24726  isppw2  25036  issqf  25057  vmasum  25136  lgsprme0  25259  gausslemma2dlem1a  25285  lgsquadlem3  25302  2lgsoddprmlem2  25329  ostth  25523  brbtwn2  25980  colinearalglem4  25984  ax5seglem1  26003  ax5seglem2  26004  axcontlem2  26040  axcontlem12  26050  upgrpredgv  26229  uhgr2edg  26295  issubgr  26358  subgrprop  26360  subuhgr  26373  subupgr  26374  subumgr  26375  subusgr  26376  nb3grprlem2  26477  cplgr3v  26537  wlk1walk  26741  upgrwlkvtxedg  26747  pthdivtx  26831  usgr2trlncl  26862  crctcshwlkn0lem3  26911  crctcshwlkn0lem6  26914  crctcshwlkn0lem7  26915  crctcshwlkn0  26920  wlkiswwlks2  26980  wwlksnextbi  27008  wwlksnfi  27020  wwlksnextprop  27026  erclwwlksym  27140  clwwlkn1  27166  clwwlkfo  27175  clwwlknwwlknclOLD  27179  erclwwlknsym  27197  clwwlknonex2lem2  27253  is0wlk  27265  is0trl  27271  3pthdlem1  27312  frgr3v  27425  frgrncvvdeqlem3  27451  frgrregorufr  27475  clwwnonrepclwwnon  27498  extwwlkfab  27507  numclwwlk1  27516  numclwlk2lem2f  27534  numclwlk2lem2f1o  27536  numclwlk2lem2fOLD  27541  numclwlk2lem2f1oOLD  27543  frgrregord013  27559  vcz  27735  isvcOLD  27739  isnv  27772  isnvi  27773  nmooge0  27927  nmblolbii  27959  blocnilem  27964  ipblnfi  28016  hvpncan2  28202  hvaddsub4  28240  hire  28256  abshicom  28263  hial2eq2  28269  orthcom  28270  hhssabloi  28424  ocsh  28447  shscli  28481  shscom  28483  shsel2  28486  spanss  28512  shjcom  28522  shmodsi  28553  chpsscon3  28667  spansni  28721  spansnmul  28728  spansncol  28732  spanunsni  28743  cmcm2  28780  cm2j  28784  spansncvi  28816  5oalem2  28819  3oalem2  28827  honegsubdi2  28975  adjsym  28997  cnvadj  29056  brafn  29111  kbpj  29120  riesz3i  29226  cnlnadjlem2  29232  cnlnadjlem9  29239  nmopcoi  29259  cnvbraval  29274  leop  29287  leop3  29289  leopmul2i  29299  leoptri  29300  hstrlem3a  29424  cvcon3  29448  cvnsym  29454  mdbr2  29460  dmdmd  29464  dmdbr2  29467  dmdbr3  29469  dmdbr4  29470  dmdbr5  29472  mdsl0  29474  ssmd2  29476  mdslmd1lem1  29489  mdslmd1lem2  29490  mdslmd3i  29496  mdslmd4i  29497  atcveq0  29512  superpos  29518  atnemeq0  29541  atssma  29542  atexch  29545  atomli  29546  atcvatlem  29549  atcvati  29550  chirredlem1  29554  chirredlem3  29556  chirredi  29558  atcvat3i  29560  atdmd  29562  mdsymlem1  29567  mdsymlem3  29569  mdsymlem4  29570  mdsymlem5  29571  mdsymlem8  29574  dmdsym  29577  atdmd2  29578  sumdmdlem  29582  cdjreui  29596  cdj3lem2b  29601  cdj3i  29605  r19.29ffa  29625  imadifxp  29717  abfmpel  29760  xaddeq0  29823  xrofsup  29838  xeqlelt  29843  xdivpnfrp  29946  xrsinvgval  29982  xrsmulgzz  29983  pcmplfin  30232  cnvordtrestixx  30264  ordtrest2NEWlem  30273  indval  30380  esumpfinvallem  30441  sigagenss  30517  ddemeas  30604  brae  30609  dya2iocival  30640  dya2iocnei  30649  dya2iocuni  30650  omsf  30663  oddpwdc  30721  bnj934  31308  derangenlem  31456  subfacval2  31472  kur14  31501  lediv2aALT  31874  dford5  31911  faclim2  31937  funpsstri  31966  dftrpred3g  32034  soseq  32056  wsuclem  32072  frrlem5  32086  elno  32101  nosepon  32120  noextenddif  32123  sltsolem1  32128  nosepne  32133  nolt02o  32147  sltnle  32180  sleloe  32181  sletri3  32182  hfelhf  32590  elicc3  32613  nn0prpwlem  32619  nn0prpw  32620  isfne  32636  onsuct0  32742  nndivsub  32758  bj-ssbequ2  32945  bj-restsnss  33338  bj-restsnss2  33339  bj-restuni2  33353  topdifinffinlem  33502  iooelexlt  33517  relowlssretop  33518  rdgeqoa  33525  wl-sbcom2d-lem1  33651  wl-sbcom2d  33653  wl-ax11-lem6  33676  curf  33696  finixpnum  33703  ltflcei  33706  leceifl  33707  cos2h  33709  matunitlindflem1  33714  matunitlindflem2  33715  matunitlindf  33716  ptrecube  33718  poimirlem6  33724  poimirlem7  33725  poimirlem10  33728  poimirlem11  33729  poimirlem27  33745  poimirlem29  33747  poimirlem30  33748  poimirlem31  33749  poimirlem32  33750  mblfinlem3  33757  mblfinlem4  33758  ismblfin  33759  ovoliunnfl  33760  voliunnfl  33762  volsupnfl  33763  cnambfre  33767  itg2addnclem2  33771  itg2addnc  33773  itg2gt0cn  33774  ftc1anclem1  33794  ftc1anclem4  33797  ftc1anclem6  33799  ftc1anclem7  33800  ftc1anc  33802  unirep  33816  opelopab3  33820  fvopabf4g  33824  indexa  33837  filbcmb  33844  incsequz2  33854  metf1o  33860  sstotbnd3  33884  isbnd2  33891  bndss  33894  ismtycnv  33910  iccbnd  33948  exidreslem  33985  exidresid  33987  ghomco  33999  isdivrngo  34058  isdrngo2  34066  rngoisocnv  34089  riscer  34096  crngohomfo  34114  unichnidl  34139  maxidlmax  34151  igenmin  34172  exmid2  34210  orel  34213  brcosscnvcoss  34508  brssr  34570  prtlem16  34654  paddss1  35602  paddss2  35603  paddss12  35604  pclfinN  35685  erngmul-rN  36600  mapdordlem2  37424  ismrc  37762  nacsfg  37766  isnacs3  37771  incssnn0  37772  mzpclall  37788  lerabdioph  37867  ltrabdioph  37870  eldioph4b  37873  jm2.17b  38026  congrep  38038  lnr2i  38184  rp-fakenanass  38358  brnonrel  38393  enrelmap  38789  enrelmapr  38790  rcompleq  38816  isotone1  38844  isotone2  38845  radcnvrat  39011  expgrowth  39032  bcc0  39037  binomcxplemnn0  39046  2sbc6g  39114  2sbc5g  39115  ordpss  39153  addrcom  39177  3impcombi  39542  sspwimp  39649  sspwimpVD  39650  ax6e2ndeqALT  39662  iunconnlem2  39666  sineq0ALT  39668  nsstr  39768  iunmapsn  39904  ssfiunibd  40018  fmul01  40311  lptre2pt  40371  stoweidlem34  40750  dirkeritg  40818  fourierdlem73  40895  smfsuplem1  41519  smfinflem  41525  sigarac  41543  2reu3  41690  afv0nbfvbi  41733  dmfcoafv  41757  cnambpcma  41815  ltnltne  41819  fzoopth  41843  elmod2  41846  pfxccatin12lem1  41929  pfxccatin12lem2  41930  pfxccatin12  41931  fmtnofac2lem  41986  prmdvdsfmtnof1lem2  42003  proththd  42037  opoeALTV  42100  opeoALTV  42101  epoo  42118  evenprm2  42129  gbegt5  42155  sbgoldbaltlem2  42174  nnsum4primeseven  42194  nnsum4primesevenALTV  42195  bgoldbtbndlem4  42202  bgoldbtbnd  42203  sprsymrelfolem2  42249  sprsymrelf1  42252  uspgrsprfo  42262  submgmcl  42300  resmgmhm2b  42306  isassintop  42352  rnghmval  42397  isrngisom  42402  c0snghm  42422  zrrnghm  42423  2zrngamgm  42445  rnghmsubcsetclem2  42482  rhmsubcsetclem2  42528  rhmsubcrngclem1  42533  rhmsubcrngclem2  42534  funcringcsetcALTV2lem9  42550  funcringcsetclem9ALTV  42573  rhmsubclem4  42595  rhmsubcALTVlem4  42613  cbvmpt2x2  42620  nn0sumltlt  42634  gsumlsscl  42670  ply1mulgsumlem1  42680  lincvalpr  42713  lincdifsn  42719  linc1  42720  lincellss  42721  islinindfiss  42745  islindeps  42748  lincresunit2  42773  islininds2  42779  lmod1zr  42788  ltsubadd2b  42812  zgtp1leeq  42817  logblt1b  42864  blengt1fldiv2p1  42893  nn0sumshdiglemB  42920  aacllem  43056
  Copyright terms: Public domain W3C validator