Theorem ancoms 448

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

Step	Hyp	Ref	Expression
1		ancoms.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	expcom 400	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 395	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

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 198  df-an 385

This theorem is referenced by:  pm3.22  449  adantl  469  sylan9bbr  502  syl2anr  586  anim12ci  603  im2anan9r  609  bi2anan9r  623  anabss4  649  anabsi7  653  anabsi8  654  syl3anr2OLD  1533  mp3anr1  1575  mp3anr2  1576  mp3anr3  1577  stoic1b  1853  dvelimf  2498  2eu3  2730  eqeqan12rd  2835  sylan9eqr  2873  r19.29vva  3280  morex  3599  sbcrext  3718  sylan9ssr  3823  pssdifcom1  4261  pssdifcom2  4262  preq12nebg  4596  opthprneg  4598  riinn0  4798  breqan12rd  4872  snopeqop  5173  propeqop  5175  soinxp  5399  frinxp  5400  seinxp  5401  brelrng  5570  dminss  5772  imainss  5773  sossfld  5805  cnvsng  5842  setlikespec  5928  ordelssne  5977  ordtri3or  5982  ordtri2  5985  ordtri4  5987  ordtr3OLD  5996  ordtri2or  6046  funsng  6161  f1co  6336  f1ocnv  6375  f1oprswap  6406  funimass4  6478  dffv2  6502  fndmdifcom  6554  fsn2  6636  fvtp2  6696  fvtp3  6697  fvtp2g  6699  fvtp3g  6700  soisoi  6812  riotaeqimp  6868  oveqan12rd  6904  brrpssg  7179  sorpsscmpl  7188  dfwe2  7221  ordsucelsuc  7262  ordunisuc2  7284  tfindsg  7300  tfindsg2  7301  dfom2  7307  funcnvuni  7359  fun11iun  7366  cofunex2g  7371  curry2  7516  soxp  7534  mpt2xopoveqd  7592  tposoprab  7633  wfr3g  7658  wfrlem5  7665  wfrlem10  7670  smores3  7696  smores2  7697  smoel  7703  dfrecs3  7715  tfr3  7741  tz7.48-2  7783  tz7.49  7786  oaordi  7873  oaword  7876  oaord1  7878  oaword2  7880  oa00  7886  oalimcl  7887  oaass  7888  oarec  7889  oacomf1o  7892  omord2  7894  omcan  7896  omword  7897  omword1  7900  omword2  7901  odi  7906  omass  7907  oneo  7908  oen0  7913  oecan  7916  oelim2  7922  nnarcl  7943  nnaordi  7945  nnaordr  7947  nnawordi  7948  nnmsucr  7952  nnmcom  7953  nnaword  7954  nnmordi  7958  nnaordex  7965  oaabslem  7970  omabslem  7973  nnneo  7978  omsmo  7981  ersym  8001  elecg  8030  riiner  8065  ecopovsym  8095  ecovcom  8099  mapvalg  8112  pmvalg  8113  elpmg  8118  elmapssres  8127  pmss12g  8129  ixpconstg  8164  ener  8249  domtr  8255  f1imaeng  8262  fundmen  8276  snmapen  8283  xpcomco  8299  xpsnen2g  8302  xpdom2  8304  xpdom1g  8306  omxpen  8311  omf1o  8312  enen2  8350  domen2  8352  sdomen2  8354  domtriord  8355  sdomel  8356  onsdominel  8358  infensuc  8387  onomeneq  8399  nndomo  8403  pssnn  8427  unbnn  8465  infcntss  8483  fiint  8486  mapfi  8511  fiin  8577  fiss  8579  infempty  8661  oiiso  8691  unwdomg  8738  suc11reg  8773  inf3lem5  8786  infeq5  8791  cantnfp1lem3  8834  r1tr  8896  r1val1  8906  rankr1ai  8918  rankonidlem  8948  onssr1  8951  djuex  9028  djuunxp  9040  tskwe  9069  carddom2  9096  carden2  9106  domtri2  9108  cardval2  9110  fidomtri  9112  fidomtri2  9113  harval2  9116  dif1card  9126  infxpenlem  9129  ac5num  9152  alephord3  9194  alephdom  9197  aleph11  9200  alephdom2  9203  cardaleph  9205  dfac3  9237  dfac5  9244  cdacomen  9298  onacda  9314  pwsdompw  9321  ackbij1lem11  9347  ackbij2  9360  cfeq0  9373  cfsuc  9374  cff1  9375  cflim2  9380  cfsmolem  9387  coftr  9390  sornom  9394  infpssrlem4  9423  ssfin4  9427  ssfin2  9437  ssfin3ds  9447  fin23lem31  9460  isf32lem9  9478  hsmexlem5  9547  axdc3lem  9567  axdc3lem2  9568  axdc3lem4  9570  zorn2lem6  9618  brdom3  9645  brdom7disj  9648  brdom6disj  9649  alephval2  9689  alephreg  9699  wuncss  9862  gruen  9929  addcompi  10011  mulcompi  10013  ltapi  10020  ltmpi  10021  nqereu  10046  addcompq  10067  addcomnq  10068  mulcompq  10069  mulcomnq  10070  ltsonq  10086  ltanq  10088  ltmnq  10089  genpnnp  10122  addcompr  10138  mulcompr  10140  ltsopr  10149  ltexprlem2  10154  prlem936  10164  suplem2pr  10170  map2psrpr  10226  axpre-ltadd  10283  xrltnle  10400  axlttri  10404  axsup  10408  ltnle  10412  letri3  10418  leloe  10419  eqlelt  10420  letric  10432  mul31  10499  subcl  10575  pncan2  10583  pncan3  10584  npcan  10585  addsubeq4  10591  npncan3  10614  negsubdi2  10635  muladd  10757  subdi  10758  mulneg2  10762  mulsub  10768  ltleadd  10806  ltsubpos  10815  posdif  10816  addge01  10833  lesub0  10840  wloglei  10855  prodgt02  11164  prodge02OLD  11166  mulsuble0b  11190  ltdivmul  11193  ledivmul  11194  lt2mul2div  11196  lerec  11201  lt2msq  11203  ltdiv23  11209  lediv23  11210  lediv2a  11212  le2msq  11218  msq11  11219  fimaxre  11263  lbreu  11268  infm3  11277  dfinfre  11299  creur  11309  creui  11310  cju  11311  nnmulcl  11340  nnmulclOLD  11341  nndivtr  11360  avgle1  11559  avgle2  11560  avgle  11561  nn0nnaddcl  11610  ltsubnn0  11630  zrevaddcl  11708  znnsub  11709  znn0sub  11710  zextlt  11737  gtndiv  11740  prime  11744  uztrn2  11942  uztric  11946  uz11  11947  nn0pzuz  11983  uzwo  11990  zmax  12024  zbtwnre  12025  rebtwnz  12026  qrevaddcl  12049  rpnnen1lem2  12053  rpnnen1lem1  12054  rpnnen1lem3  12055  rpnnen1lem5  12057  difrp  12102  xrltnsym  12206  xrlttri  12208  xrleloe  12213  xrletri  12222  xrletri3  12223  xrmaxeq  12248  xrmineq  12249  xrmaxlt  12250  xrmaxle  12252  lemaxle  12264  z2ge  12267  qbtwnre  12268  qextlt  12272  qextle  12273  xleneg  12287  xaddcom  12309  xmulcom  12334  xmulneg2  12338  xmulgt0  12351  xrsupsslem  12375  xrinfmsslem  12376  supxrunb1  12387  supxrunb2  12388  ixxssixx  12427  ixxin  12430  ioon0  12439  iccid  12458  iooshf  12490  iccsupr  12505  iooneg  12533  iccneg  12534  iccsplit  12548  fzen  12601  fzadd2  12619  fzass4  12622  fzrev  12646  fznn  12651  elfzp1b  12660  elfzm1b  12661  fz0fzdiffz0  12692  difelfznle  12697  fzon  12733  fzo0n  12734  fzonmapblen  12758  elfzoext  12769  eluzgtdifelfzo  12774  ubmelm1fzo  12808  elfzom1elp1fzo1  12812  subfzo0  12834  fllt  12851  flflp1  12852  flbi  12861  flbi2  12862  flzadd  12871  ltdifltdiv  12879  dfceil2  12884  modcyc2  12950  modifeq2int  12976  modaddmodup  12977  modaddmodlo  12978  modfzo0difsn  12986  modsumfzodifsn  12987  om2uzlt2i  12994  om2uzf1oi  12996  fseqsupubi  13021  fsuppmapnn0fiub0  13036  expcllem  13114  mulbinom2  13227  faclbnd5  13325  hashbnd  13363  hasheni  13376  hasheqf1oi  13380  hashdom  13406  hashss  13434  hashfacen  13475  ccatsymb  13599  ccatass  13605  ccatalpha  13610  wrd2ind  13721  swrdccatin12lem2b  13730  swrdccatin2  13731  swrdccatin12lem2  13733  swrdccatin12  13735  swrdccat3blem  13739  swrdccatid  13741  repswsymball  13770  repswsymballbi  13771  cshwsublen  13786  cshwn  13787  cshwlen  13789  cshwidxmod  13793  cshf1  13800  repswcshw  13802  cshweqdif2  13809  cshweqrep  13811  cshwcsh2id  13818  ccatco  13825  swrdco  13827  lswco  13828  s3iunsndisj  13952  relexprelg  14021  relexpnndm  14024  relexpaddnn  14034  shftlem  14051  shftuz  14052  shftfval  14053  shftval4  14060  shftval5  14061  2shfti  14063  seqshft  14068  mulre  14104  sqrtlt  14245  abs3dif  14314  abs2difabs  14317  uzin2  14327  rexanre  14329  caubnd  14341  climshftlem  14548  rlimcn2  14564  fsumcnv  14747  modfsummods  14767  geo2lim  14848  ntrivcvgfvn0  14872  prodmo  14907  zprod  14908  prodss  14918  fprodcnv  14954  bpolysum  15024  bpoly4  15030  efle  15088  reef11  15089  demoivre  15170  demoivreALT  15171  znnenlemOLD  15180  sqrt2irr  15219  nndivides  15233  0dvds  15245  muldvds1  15249  muldvds2  15250  dvdscmulr  15253  dvdssubr  15270  dvdsadd2b  15271  odd2np1  15305  mulsucdiv2z  15317  ltoddhalfle  15325  divalglem9  15364  ndvdssub  15372  gcdcllem1  15460  gcdcom  15474  neggcd  15483  gcdabs2  15491  modgcd  15492  lcmcom  15545  neglcm  15556  lcmgcdeq  15564  coprmdvds  15605  qredeq  15609  divgcdcoprmex  15618  dvdsprm  15652  cncongrprm  15674  odzdvds  15737  powm2modprm  15745  modprmn0modprm0  15749  coprimeprodsq  15750  pythagtriplem1  15758  pythagtriplem4  15761  pc2dvds  15820  pc11  15821  pcz  15822  pcprod  15836  prmunb  15855  1arithlem3  15866  1arith  15868  cshwshashlem2  16035  cshwshashlem3  16036  ressabs  16171  acsfn2  16548  issect  16637  funcestrcsetclem9  17013  funcsetcestrclem5  17024  funcsetcestrclem9  17028  pospo  17198  latjcom  17284  latmcom  17300  clatglbss  17352  pospropd  17359  pslem  17431  tsrss  17448  issubmnd  17543  submcl  17578  resmhm2b  17586  frmdmnd  17621  frmd0  17622  grpinvsub  17722  dfgrp3lem  17738  gimcnv  17931  gimco  17932  gictr  17939  cntz2ss  17986  cntzrec  17987  symg2bas  18039  symgextf1  18062  symgfixelsi  18076  pmtrfinv  18102  pmtrdifwrdel2  18127  dfod2  18202  lsmcom2  18291  efgred  18382  qusabl  18489  cygabl  18513  gsummptnn0fz  18603  gsummptnn0fzOLD  18604  eldprd  18625  srgmulgass  18753  dfrhm2  18941  isrim0  18947  rmodislmodlem  19154  rmodislmod  19155  lmimcnv  19294  mplcoe5lem  19696  psrbagfsupp  19737  cnfldexp  20007  cnsrng  20008  xrsdsreval  20019  dvdsrzring  20059  znf1o  20127  ocvocv  20246  ocvin  20249  frlmip  20348  islindf  20382  lindff  20385  lindfrn  20391  f1lindf  20392  mamudir  20441  matsca2  20457  matbas2  20458  matlmod  20466  matinvgcell  20472  mat1bas  20487  dmatmul  20535  dmatsgrp  20537  dmatsrng  20539  dmatcrng  20540  scmatsgrp1  20560  scmatsrng1  20561  madulid  20683  gsummatr01lem3  20696  gsummatr01  20698  cpmatacl  20755  0mat2pmat  20775  idmatidpmat  20776  m2cpminv0  20800  pmatcollpw3fi1lem1  20825  chfacfscmulgsum  20899  chfacfpmmulgsum  20903  eltg  20996  eltg2  20997  tgss  21007  tgss2  21026  basgen2  21028  bastop1  21032  cldmre  21117  toponmre  21132  opnneiss  21157  restcldr  21213  restfpw  21218  restcls  21220  restntr  21221  ordtbaslem  21227  ordtrest2lem  21242  leordtvallem2  21250  leordtval  21252  cnrest  21324  t0sep  21363  cmpcov  21427  cmpsublem  21437  cmpsub  21438  bwth  21448  2ndcomap  21496  locfincmp  21564  ptval  21608  xkoval  21625  txss12  21643  ptrescn  21677  xkopt  21693  hmeofval  21796  txswaphmeolem  21842  txswaphmeo  21843  trfbas2  21881  trfbas  21882  uzrest  21935  numufl  21953  ssufl  21956  flimclsi  22016  hauspwpwf1  22025  ghmcnp  22152  blpnfctr  22475  metequiv  22548  metcnp3  22579  elbl4  22602  restmetu  22609  tngngp  22692  qtopbaslem  22796  bl2ioo  22829  ioo2bl  22830  ioo2blex  22831  xrsxmet  22846  divccn  22910  divccncf  22943  isclmi0  23131  iscvsi  23162  causs  23330  lmclim  23335  bcthlem1  23355  ovolfsf  23475  ioombl  23569  iccvolcl  23571  ioovolcl  23574  ioorcl  23581  volcn  23610  itg2itg1  23740  dvexp  23953  dvmptfsum  23975  dvexp3  23978  dvef  23980  dvlip  23993  c1lip1  23997  ftc1a  24037  tdeglem1  24055  tdeglem3  24056  tdeglem4  24057  coe1termlem  24251  plyremlem  24296  ptolemy  24486  cos11  24517  logeftb  24567  logleb  24586  logdivlt  24604  logdivle  24605  angval  24768  isppw2  25078  issqf  25099  vmasum  25178  lgsprme0  25301  gausslemma2dlem1a  25327  lgsquadlem3  25344  2lgsoddprmlem2  25371  ostth  25565  brbtwn2  26022  colinearalglem4  26026  ax5seglem1  26045  ax5seglem2  26046  axcontlem2  26082  axcontlem12  26092  upgrpredgv  26272  uhgr2edg  26338  issubgr  26402  subgrprop  26404  subuhgr  26417  subupgr  26418  subumgr  26419  subusgr  26420  nb3grprlem2  26522  cplgr3v  26582  wlk1walk  26786  upgrwlkvtxedg  26792  pthdivtx  26876  usgr2trlncl  26907  crctcshwlkn0lem3  26956  crctcshwlkn0lem6  26959  crctcshwlkn0lem7  26960  crctcshwlkn0  26965  wlkiswwlks2  27025  wwlksnextbi  27054  wwlksnfi  27066  wwlksnextprop  27073  erclwwlksym  27187  clwwlkn1  27213  clwwlkfo  27222  clwwlknwwlknclOLD  27226  erclwwlknsym  27244  clwwlknonex2lem2  27300  is0wlk  27313  is0trl  27319  3pthdlem1  27360  frgr3v  27473  frgrncvvdeqlem3  27499  frgrregorufr  27523  clwwnonrepclwwnon  27545  extwwlkfab  27554  numclwwlk1  27564  numclwlk2lem2f  27580  numclwlk2lem2f1o  27582  numclwlk2lem2fOLD  27587  numclwlk2lem2f1oOLD  27589  frgrregord013  27606  vcz  27781  isvcOLD  27785  isnv  27818  isnvi  27819  nmooge0  27973  nmblolbii  28005  blocnilem  28010  ipblnfi  28062  hvpncan2  28248  hvaddsub4  28286  hire  28302  abshicom  28309  hial2eq2  28315  orthcom  28316  hhssabloi  28470  ocsh  28493  shscli  28527  shscom  28529  shsel2  28532  spanss  28558  shjcom  28568  shmodsi  28599  chpsscon3  28713  spansni  28767  spansnmul  28774  spansncol  28778  spanunsni  28789  cmcm2  28826  cm2j  28830  spansncvi  28862  5oalem2  28865  3oalem2  28873  honegsubdi2  29021  adjsym  29043  cnvadj  29102  brafn  29157  kbpj  29166  riesz3i  29272  cnlnadjlem2  29278  cnlnadjlem9  29285  nmopcoi  29305  cnvbraval  29320  leop  29333  leop3  29335  leopmul2i  29345  leoptri  29346  hstrlem3a  29470  cvcon3  29494  cvnsym  29500  mdbr2  29506  dmdmd  29510  dmdbr2  29513  dmdbr3  29515  dmdbr4  29516  dmdbr5  29518  mdsl0  29520  ssmd2  29522  mdslmd1lem1  29535  mdslmd1lem2  29536  mdslmd3i  29542  mdslmd4i  29543  atcveq0  29558  superpos  29564  atnemeq0  29587  atssma  29588  atexch  29591  atomli  29592  atcvatlem  29595  atcvati  29596  chirredlem1  29600  chirredlem3  29602  chirredi  29604  atcvat3i  29606  atdmd  29608  mdsymlem1  29613  mdsymlem3  29615  mdsymlem4  29616  mdsymlem5  29617  mdsymlem8  29620  dmdsym  29623  atdmd2  29624  sumdmdlem  29628  cdjreui  29642  cdj3lem2b  29647  cdj3i  29651  r19.29ffa  29671  imadifxp  29762  abfmpel  29805  xaddeq0  29868  xrofsup  29883  xeqlelt  29888  xdivpnfrp  29989  xrsinvgval  30025  xrsmulgzz  30026  pcmplfin  30275  cnvordtrestixx  30307  ordtrest2NEWlem  30316  indval  30423  esumpfinvallem  30484  sigagenss  30560  ddemeas  30647  brae  30652  dya2iocival  30683  dya2iocnei  30692  dya2iocuni  30693  omsf  30706  oddpwdc  30764  bnj934  31350  derangenlem  31498  subfacval2  31514  kur14  31543  lediv2aALT  31915  dford5  31952  faclim2  31978  funpsstri  32007  dftrpred3g  32075  soseq  32097  wsuclem  32113  frrlem5  32127  elno  32142  nosepon  32161  noextenddif  32164  sltsolem1  32169  nosepne  32174  nolt02o  32188  sltnle  32221  sleloe  32222  sletri3  32223  hfelhf  32631  elicc3  32654  nn0prpwlem  32660  nn0prpw  32661  isfne  32677  onsuct0  32779  nndivsub  32795  bj-ssbequ2  32980  bj-restsnss  33366  bj-restsnss2  33367  bj-restuni2  33381  topdifinffinlem  33530  iooelexlt  33545  relowlssretop  33546  rdgeqoa  33553  wl-sbcom2d-lem1  33675  wl-sbcom2d  33677  wl-ax11-lem6  33700  curf  33719  finixpnum  33726  ltflcei  33729  leceifl  33730  cos2h  33732  matunitlindflem1  33737  matunitlindflem2  33738  matunitlindf  33739  ptrecube  33741  poimirlem6  33747  poimirlem7  33748  poimirlem10  33751  poimirlem11  33752  poimirlem27  33768  poimirlem29  33770  poimirlem30  33771  poimirlem31  33772  poimirlem32  33773  mblfinlem3  33780  mblfinlem4  33781  ismblfin  33782  ovoliunnfl  33783  voliunnfl  33785  volsupnfl  33786  cnambfre  33789  itg2addnclem2  33793  itg2addnc  33795  itg2gt0cn  33796  ftc1anclem1  33816  ftc1anclem4  33819  ftc1anclem6  33821  ftc1anclem7  33822  ftc1anc  33824  unirep  33838  opelopab3  33842  fvopabf4g  33846  indexa  33859  filbcmb  33866  incsequz2  33875  metf1o  33881  sstotbnd3  33905  isbnd2  33912  bndss  33915  ismtycnv  33931  iccbnd  33969  exidreslem  34006  exidresid  34008  ghomco  34020  isdivrngo  34079  isdrngo2  34087  rngoisocnv  34110  riscer  34117  crngohomfo  34135  unichnidl  34160  maxidlmax  34172  igenmin  34193  exmid2  34231  orel  34234  brcosscnvcoss  34521  brssr  34583  prtlem16  34667  paddss1  35616  paddss2  35617  paddss12  35618  pclfinN  35699  erngmul-rN  36613  mapdordlem2  37436  ismrc  37784  nacsfg  37788  isnacs3  37793  incssnn0  37794  mzpclall  37810  lerabdioph  37889  ltrabdioph  37892  eldioph4b  37895  jm2.17b  38047  congrep  38059  lnr2i  38205  rp-fakenanass  38378  brnonrel  38413  enrelmap  38809  enrelmapr  38810  rcompleq  38836  isotone1  38864  isotone2  38865  radcnvrat  39031  expgrowth  39052  bcc0  39057  binomcxplemnn0  39066  2sbc6g  39133  2sbc5g  39134  ordpss  39171  addrcom  39195  3impcombi  39559  sspwimp  39666  sspwimpVD  39667  ax6e2ndeqALT  39679  iunconnlem2  39683  sineq0ALT  39685  nsstr  39784  iunmapsn  39914  ssfiunibd  40022  fmul01  40310  lptre2pt  40370  stoweidlem34  40748  dirkeritg  40816  fourierdlem73  40893  smfsuplem1  41517  smfinflem  41523  sigarac  41541  2reu3  41718  fundmdfat  41736  dfatelrn  41738  afv0nbfvbi  41758  dmfcoafv  41782  dfatcolem  41862  cnambpcma  41903  ltnltne  41907  fzoopth  41930  elmod2  41933  pfxccatin12lem1  42016  pfxccatin12lem2  42017  pfxccatin12  42018  fmtnofac2lem  42073  prmdvdsfmtnof1lem2  42090  proththd  42124  opoeALTV  42187  opeoALTV  42188  epoo  42205  evenprm2  42216  gbegt5  42242  sbgoldbaltlem2  42261  nnsum4primeseven  42281  nnsum4primesevenALTV  42282  bgoldbtbndlem4  42289  bgoldbtbnd  42290  sprsymrelfolem2  42329  sprsymrelf1  42332  uspgrsprfo  42342  submgmcl  42380  resmgmhm2b  42386  isassintop  42432  rnghmval  42477  isrngisom  42482  c0snghm  42502  zrrnghm  42503  2zrngamgm  42525  rnghmsubcsetclem2  42562  rhmsubcsetclem2  42608  rhmsubcrngclem1  42613  rhmsubcrngclem2  42614  funcringcsetcALTV2lem9  42630  funcringcsetclem9ALTV  42653  rhmsubclem4  42675  rhmsubcALTVlem4  42693  cbvmpt2x2  42700  nn0sumltlt  42714  gsumlsscl  42750  ply1mulgsumlem1  42760  lincvalpr  42793  lincdifsn  42799  linc1  42800  lincellss  42801  islinindfiss  42825  islindeps  42828  lincresunit2  42853  islininds2  42859  lmod1zr  42868  ltsubadd2b  42892  zgtp1leeq  42897  logblt1b  42944  blengt1fldiv2p1  42973  nn0sumshdiglemB  43000  aacllem  43136