Theorem ancoms 268

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 116	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 124	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  adantl  277  syl2anr  290  anim12ci  339  sylan9bbr  463  anabss4  577  anabsi7  581  anabsi8  582  im2anan9r  601  bi2anan9r  609  syl3anr2  1305  mp3anr1  1349  mp3anr2  1350  mp3anr3  1351  stoic1b  1450  cbvaldvaw  1957  eu5  2105  2exeu  2150  eqeqan12rd  2226  sylan9eqr  2264  r19.29vva  2656  morex  2967  sylan9ssr  3218  riinm  4017  breqan12rd  4079  elnn  4675  soinxp  4766  seinxp  4767  brelrng  4931  dminss  5119  imainss  5120  funsng  5343  funcnvuni  5366  f1co  5519  f1ocnv  5561  fun11iun  5569  funimass4  5657  fndmdifcom  5714  fsn2  5782  fvtp2g  5821  fvtp3g  5822  fvtp2  5824  fvtp3  5825  riotaeqimp  5952  acexmid  5973  oveqan12rd  5994  cofunex2g  6225  brtposg  6370  tposoprab  6396  smores3  6409  smores2  6410  smoel  6416  tfri3  6483  rdgtfr  6490  rdgruledefgg  6491  omcl  6577  oeicl  6578  nnmsucr  6604  nnmcom  6605  nndir  6606  nnaordi  6624  nnaordr  6626  nnaword  6627  nnmordi  6632  nnaordex  6644  nnm00  6646  ersym  6662  elecg  6690  riinerm  6725  ecopovsym  6748  ecopovsymg  6751  ecovcom  6759  ecovicom  6760  mapvalg  6775  pmvalg  6776  elpmg  6781  elmapssres  6790  pmss12g  6792  ixpconstg  6824  domssr  6899  ener  6901  domtr  6907  f1imaeng  6914  fundmen  6929  xpcomco  6953  xpsnen2g  6956  xpdom2  6958  xpdom1g  6960  enen2  6970  domen2  6972  ssfilem  7005  diffitest  7017  fiintim  7061  fundmfibi  7073  cnvti  7154  djuex  7178  nnnninf  7261  netap  7408  2omotaplemap  7411  ltsopi  7475  pitric  7476  pitri3or  7477  addcompig  7484  mulcompig  7486  ltapig  7493  ltmpig  7494  nnppipi  7498  addcomnqg  7536  addassnqg  7537  distrnqg  7542  recexnq  7545  nqtri3or  7551  ltmnqg  7556  lt2addnq  7559  lt2mulnq  7560  ltbtwnnqq  7570  prarloclemarch2  7574  enq0ref  7588  distrnq0  7614  mulcomnq0  7615  prcdnql  7639  prcunqu  7640  prarloclemlt  7648  genpassl  7679  genpassu  7680  nqprloc  7700  nqpru  7707  appdiv0nq  7719  addcomprg  7733  mulcomprg  7735  distrlem4prl  7739  distrlem4pru  7740  1idprl  7745  1idpru  7746  ltsopr  7751  recexprlemss1l  7790  recexprlemss1u  7791  gt0srpr  7903  mulcomsrg  7912  ltsosr  7919  aptisr  7934  mulextsr1  7936  map2psrprg  7960  axaddcom  8025  axltwlin  8182  axapti  8185  letri3  8195  eqlelt  8201  mul31  8245  cnegexlem3  8291  subval  8306  subcl  8313  pncan2  8321  pncan3  8322  npcan  8323  addsubeq4  8329  npncan3  8352  negsubdi2  8373  muladd  8498  subdi  8499  mulneg2  8510  mulsub  8515  ltleadd  8561  ltsubpos  8569  posdif  8570  addge01  8587  lesub0  8594  reapneg  8712  prodgt02  8968  prodge02  8970  ltdivmul  8991  lerec  8999  lediv2a  9010  le2msq  9016  msq11  9017  lbreu  9060  dfinfre  9071  creur  9074  creui  9075  cju  9076  nnmulcl  9099  nndivtr  9120  avgle1  9320  avgle2  9321  nn0nnaddcl  9368  zletric  9458  zrevaddcl  9465  znnsub  9466  znn0sub  9480  ltsubnn0  9482  zdclt  9492  zextlt  9507  gtndiv  9510  prime  9514  peano5uzti  9523  uztrn2  9708  uztric  9712  uz11  9713  nn0pzuz  9750  indstr  9756  supinfneg  9758  infsupneg  9759  eluzdc  9773  qrevaddcl  9807  difrp  9856  xrltnsym  9957  xrltso  9960  xrlttri3  9961  xrletri3  9968  xleneg  10001  xaddcom  10025  xposdif  10046  ixxssixx  10066  iccid  10089  iooshf  10116  iccsupr  10130  iooneg  10152  iccneg  10153  fztri3or  10203  fzdcel  10204  fzn  10206  fzen  10207  fzass4  10226  fzrev  10248  fznn  10253  elfzp1b  10261  elfzm1b  10262  fz0fzdiffz0  10294  difelfznle  10299  fzon  10331  fzo0n  10332  fzonmapblen  10355  elfzoextl  10364  eluzgtdifelfzo  10370  ubmelm1fzo  10399  subfzo0  10415  qletric  10428  qdclt  10432  qdcle  10433  ioo0  10446  ico0  10448  ioc0  10449  flqbi  10477  flqbi2  10478  flqzadd  10485  modfzo0difsn  10584  fzfig  10619  expcllem  10739  expap0  10758  mulbinom2  10845  expnbnd  10852  sq11ap  10896  hashfacen  11025  iswrdinn0  11043  ccatsymb  11103  swrd0g  11158  swrdsbslen  11164  swrdspsleq  11165  wrd2ind  11221  pfxccatin12lem1  11226  pfxccatin12lem2  11229  pfxccatin12  11231  swrdccat3blem  11237  shftlem  11293  shftuz  11294  shftfvalg  11295  ovshftex  11296  shftfval  11298  shftval4  11305  shftval5  11306  2shfti  11308  mulreap  11341  sqrt11ap  11515  abs3dif  11582  abs2difabs  11585  maxabslemval  11685  maxle2  11689  maxclpr  11699  2zsupmax  11703  mingeb  11719  2zinfmin  11720  xrmaxiflemval  11727  xrmax2sup  11731  iooinsup  11754  climshftlemg  11779  fsumcnv  11914  explecnv  11982  geo2lim  11993  prodmodc  12055  fprodcnv  12102  demoivre  12250  demoivreALT  12251  nndivides  12274  0dvds  12288  muldvds1  12293  muldvds2  12294  dvdssubr  12316  dvdsadd2b  12317  odd2np1  12350  mulsucdiv2z  12362  ltoddhalfle  12370  ndvdssub  12407  gcdcom  12460  neggcd  12470  gcdabs2  12477  modgcd  12478  bezoutlemaz  12490  dfgcd2  12501  lcmcom  12552  neglcm  12563  lcmgcdeq  12571  coprmdvds  12580  qredeq  12584  divgcdcoprmex  12590  isprm3  12606  prmind2  12608  dvdsprm  12625  cncongrprm  12645  sqrt2irr  12650  hashgcdeq  12728  modprmn0modprm0  12745  coprimeprodsq  12746  pythagtriplem1  12754  pythagtriplem4  12757  pc2dvds  12819  pc11  12820  pcz  12821  pcprod  12835  prmunb  12851  1arithlem2  12853  1arithlem3  12854  1arith  12856  ptex  13263  issubmnd  13441  submcl  13478  resmhm2b  13488  grpinvsub  13581  dfgrp3mlem  13597  imasabl  13839  mgpress  13860  srgmulgass  13918  dfrhm2  14083  isrim0  14090  rmodislmodlem  14279  rmodislmod  14280  cnfldexp  14506  dvdsrzring  14532  znf1o  14580  eltg  14691  eltg2  14692  tgss  14702  tgss2  14718  basgen2  14720  bastop1  14722  opnneiss  14797  cnrest  14874  txss12  14905  hmeofvalg  14942  txswaphmeolem  14959  txswaphmeo  14960  blpnfctr  15078  metequiv  15134  metcnp3  15150  qtopbasss  15160  reopnap  15185  bl2ioo  15189  ioo2bl  15190  ioo2blex  15191  cncfval  15211  divccncfap  15229  addccncf  15239  expcncf  15248  dvexp  15350  dvmptfsum  15364  dvef  15366  efle  15415  reapef  15417  ptolemy  15463  logleb  15514  lgsprme0  15686  gausslemma2dlem1a  15702  gausslemma2dlem4  15708  lgsquadlem3  15723  2lgsoddprmlem2  15750  upgrpredgv  15909  uhgr2edg  15969  uzdcinzz  16072  exmidsbthrlem  16301  triap  16308