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  467  anabss4  583  anabsi7  587  anabsi8  588  im2anan9r  607  bi2anan9r  615  syl3anr2  1331  mp3anr1  1375  mp3anr2  1376  mp3anr3  1377  stoic1b  1477  cbvaldvaw  1986  eu5  2134  2exeu  2179  eqeqan12rd  2255  sylan9eqr  2293  r19.29vva  2696  morex  3010  sylan9ssr  3262  riinm  4083  breqan12rd  4145  elnn  4751  soinxp  4843  seinxp  4844  brelrng  5011  dminss  5200  imainss  5201  funsng  5425  funcnvuni  5448  f1co  5608  f1ocnv  5650  fun11iun  5658  funimass4  5750  fndmdifcom  5809  fsn2  5876  fvtp2g  5918  fvtp3g  5919  fvtp2  5921  fvtp3  5922  riotaeqimp  6057  acexmid  6078  oveqan12rd  6099  cofunex2g  6333  brtposg  6519  tposoprab  6545  smores3  6558  smores2  6559  smoel  6565  tfri3  6632  rdgtfr  6639  rdgruledefgg  6640  omcl  6728  oeicl  6729  nnmsucr  6755  nnmcom  6756  nndir  6757  nnaordi  6775  nnaordr  6777  nnaword  6778  nnmordi  6783  nnaordex  6795  nnm00  6797  ersym  6813  elecg  6841  riinerm  6876  ecopovsym  6899  ecopovsymg  6902  ecovcom  6910  ecovicom  6911  mapvalg  6926  pmvalg  6927  elpmg  6932  elmapssres  6948  pmss12g  6950  ixpconstg  6983  domssr  7058  ener  7060  domtr  7066  f1imaeng  7073  fundmen  7088  xpcomco  7118  xpsnen2g  7121  xpdom2  7123  xpdom1g  7125  enen2  7135  domen2  7137  ssfilem  7171  ssfilemd  7173  diffitest  7185  fiintim  7232  fundmfibi  7246  f1setfi  7311  cnvti  7353  djuex  7377  nnnninf  7460  netap  7614  2omotaplemap  7617  ltsopi  7681  pitric  7682  pitri3or  7683  addcompig  7690  mulcompig  7692  ltapig  7699  ltmpig  7700  nnppipi  7704  addcomnqg  7742  addassnqg  7743  distrnqg  7748  recexnq  7751  nqtri3or  7757  ltmnqg  7762  lt2addnq  7765  lt2mulnq  7766  ltbtwnnqq  7776  prarloclemarch2  7780  enq0ref  7794  distrnq0  7820  mulcomnq0  7821  prcdnql  7845  prcunqu  7846  prarloclemlt  7854  genpassl  7885  genpassu  7886  nqprloc  7906  nqpru  7913  appdiv0nq  7925  addcomprg  7939  mulcomprg  7941  distrlem4prl  7945  distrlem4pru  7946  1idprl  7951  1idpru  7952  ltsopr  7957  recexprlemss1l  7996  recexprlemss1u  7997  gt0srpr  8109  mulcomsrg  8118  ltsosr  8125  aptisr  8140  mulextsr1  8142  map2psrprg  8166  axaddcom  8231  axltwlin  8387  axapti  8390  letri3  8400  eqlelt  8406  mul31  8451  cnegexlem3  8497  subval  8512  subcl  8519  pncan2  8527  pncan3  8528  npcan  8529  addsubeq4  8535  npncan3  8558  negsubdi2  8579  muladd  8705  subdi  8706  mulneg2  8717  mulsub  8722  ltleadd  8768  ltsubpos  8776  posdif  8777  addge01  8794  lesub0  8801  reapneg  8919  prodgt02  9177  prodge02  9179  ltdivmul  9200  lerec  9208  lediv2a  9219  le2msq  9225  msq11  9226  lbreu  9269  dfinfre  9280  creur  9283  creui  9284  cju  9285  nnmulcl  9308  nndivtr  9329  avgle1  9529  avgle2  9530  nn0nnaddcl  9577  zletric  9671  zrevaddcl  9678  znnsub  9679  znn0sub  9693  ltsubnn0  9695  zdclt  9705  zextlt  9721  gtndiv  9724  prime  9728  peano5uzti  9737  uztrn2  9923  uztric  9927  uz11  9928  nn0pzuz  9970  indstr  9976  supinfneg  9978  infsupneg  9979  eluzdc  9993  qrevaddcl  10027  difrp  10076  xrltnsym  10178  xrltso  10181  xrlttri3  10182  xrletri3  10189  xleneg  10222  xaddcom  10246  xposdif  10267  ixxssixx  10287  iccid  10310  iooshf  10337  iccsupr  10351  iooneg  10373  iccneg  10374  fztri3or  10426  fzdcel  10427  fzn  10429  fzen  10430  fzass4  10451  fzrev  10474  fznn  10479  elfzp1b  10487  elfzm1b  10488  fz0fzdiffz0  10520  difelfznle  10525  fzon  10557  fzo0n  10558  fzonmapblen  10582  elfzoextl  10592  eluzgtdifelfzo  10598  ubmelm1fzo  10627  subfzo0  10644  qletric  10659  qdclt  10663  qdcle  10664  ioo0  10677  ico0  10679  ioc0  10680  flqbi  10708  flqbi2  10709  flqzadd  10716  modfzo0difsn  10815  fzfig  10850  expcllem  10970  expap0  10989  mulbinom2  11076  expnbnd  11084  sq11ap  11128  hashfacen  11267  iswrdinn0  11292  ccatsymb  11353  ccatalpha  11364  swrd0g  11415  swrdsbslen  11421  swrdspsleq  11422  wrd2ind  11478  pfxccatin12lem1  11483  pfxccatin12lem2  11486  pfxccatin12  11488  swrdccat3blem  11494  shftlem  11564  shftuz  11565  shftfvalg  11566  ovshftex  11567  shftfval  11569  shftval4  11576  shftval5  11577  2shfti  11579  mulreap  11612  sqrt11ap  11787  abs3dif  11854  abs2difabs  11857  maxabslemval  11957  maxle2  11961  maxclpr  11971  2zsupmax  11975  mingeb  11991  2zinfmin  11992  xrmaxiflemval  11999  xrmax2sup  12003  iooinsup  12026  climshftlemg  12051  fsumcnv  12187  explecnv  12255  geo2lim  12266  prodmodc  12328  fprodcnv  12375  demoivre  12523  demoivreALT  12524  nndivides  12547  0dvds  12561  muldvds1  12566  muldvds2  12567  dvdssubr  12589  dvdsadd2b  12590  odd2np1  12623  mulsucdiv2z  12635  ltoddhalfle  12643  ndvdssub  12680  gcdcom  12733  neggcd  12743  gcdabs2  12750  modgcd  12751  bezoutlemaz  12763  dfgcd2  12774  lcmcom  12825  neglcm  12836  lcmgcdeq  12844  coprmdvds  12853  qredeq  12857  divgcdcoprmex  12863  isprm3  12879  prmind2  12881  dvdsprm  12898  cncongrprm  12918  sqrt2irr  12923  hashgcdeq  13001  modprmn0modprm0  13018  coprimeprodsq  13019  pythagtriplem1  13027  pythagtriplem4  13030  pc2dvds  13092  pc11  13093  pcz  13094  pcprod  13108  prmunb  13124  1arithlem2  13126  1arithlem3  13127  1arith  13129  ptex  13601  issubmnd  13738  submcl  13769  resmhm2b  13779  grpinvsub  13870  dfgrp3mlem  13886  imasabl  14123  mgpress  14213  srgmulgass  14276  dfrhm2  14444  isrim0  14451  rmodislmodlem  14670  rmodislmod  14671  cnfldexp  14897  dvdsrzring  14921  znf1o  14969  eltg  15136  eltg2  15137  tgss  15147  tgss2  15163  basgen2  15165  bastop1  15167  opnneiss  15242  cnrest  15319  txss12  15350  hmeofvalg  15387  txswaphmeolem  15404  txswaphmeo  15405  blpnfctr  15523  metequiv  15579  metcnp3  15595  qtopbasss  15605  reopnap  15630  bl2ioo  15634  ioo2bl  15635  ioo2blex  15636  cncfval  15656  divccncfap  15674  addccncf  15684  expcncf  15693  dvexp  15795  dvmptfsum  15809  dvef  15811  efle  15860  reapef  15862  ptolemy  15908  logleb  15959  lgsprme0  16144  gausslemma2dlem1a  16160  gausslemma2dlem4  16166  lgsquadlem3  16181  2lgsoddprmlem2  16208  upgrpredgv  16370  uhgr2edg  16430  issubgr  16481  subgrprop  16483  subuhgr  16496  subupgr  16497  subumgr  16498  subusgr  16499  upgriswlkdc  16584  upgrwlkvtxedg  16588  g0wlk0  16594  clwwlkn1  16642  clwwlknonex2lem2  16662  dichmul0orlem3  16738  uzdcinzz  16809  exmidsbthrlem  17041  triap  17052