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  599  bi2anan9r  607  syl3anr2  1302  mp3anr1  1345  mp3anr2  1346  mp3anr3  1347  stoic1b  1439  eu5  2085  2exeu  2130  eqeqan12rd  2206  sylan9eqr  2244  r19.29vva  2635  morex  2936  sylan9ssr  3184  riinm  3974  breqan12rd  4035  elnn  4623  soinxp  4714  seinxp  4715  brelrng  4876  dminss  5061  imainss  5062  funsng  5281  funcnvuni  5304  f1co  5452  f1ocnv  5493  fun11iun  5501  funimass4  5587  fndmdifcom  5643  fsn2  5711  fvtp2g  5746  fvtp3g  5747  fvtp2  5749  fvtp3  5750  acexmid  5895  oveqan12rd  5916  cofunex2g  6135  brtposg  6279  tposoprab  6305  smores3  6318  smores2  6319  smoel  6325  tfri3  6392  rdgtfr  6399  rdgruledefgg  6400  omcl  6486  oeicl  6487  nnmsucr  6513  nnmcom  6514  nndir  6515  nnaordi  6533  nnaordr  6535  nnaword  6536  nnmordi  6541  nnaordex  6553  nnm00  6555  ersym  6571  elecg  6599  riinerm  6634  ecopovsym  6657  ecopovsymg  6660  ecovcom  6668  ecovicom  6669  mapvalg  6684  pmvalg  6685  elpmg  6690  elmapssres  6699  pmss12g  6701  ixpconstg  6733  ener  6805  domtr  6811  f1imaeng  6818  fundmen  6832  xpcomco  6852  xpsnen2g  6855  xpdom2  6857  xpdom1g  6859  enen2  6869  domen2  6871  ssfilem  6903  diffitest  6915  fiintim  6957  fundmfibi  6968  cnvti  7048  djuex  7072  nnnninf  7154  netap  7283  2omotaplemap  7286  ltsopi  7349  pitric  7350  pitri3or  7351  addcompig  7358  mulcompig  7360  ltapig  7367  ltmpig  7368  nnppipi  7372  addcomnqg  7410  addassnqg  7411  distrnqg  7416  recexnq  7419  nqtri3or  7425  ltmnqg  7430  lt2addnq  7433  lt2mulnq  7434  ltbtwnnqq  7444  prarloclemarch2  7448  enq0ref  7462  distrnq0  7488  mulcomnq0  7489  prcdnql  7513  prcunqu  7514  prarloclemlt  7522  genpassl  7553  genpassu  7554  nqprloc  7574  nqpru  7581  appdiv0nq  7593  addcomprg  7607  mulcomprg  7609  distrlem4prl  7613  distrlem4pru  7614  1idprl  7619  1idpru  7620  ltsopr  7625  recexprlemss1l  7664  recexprlemss1u  7665  gt0srpr  7777  mulcomsrg  7786  ltsosr  7793  aptisr  7808  mulextsr1  7810  map2psrprg  7834  axaddcom  7899  axltwlin  8055  axapti  8058  letri3  8068  eqlelt  8074  mul31  8118  cnegexlem3  8164  subval  8179  subcl  8186  pncan2  8194  pncan3  8195  npcan  8196  addsubeq4  8202  npncan3  8225  negsubdi2  8246  muladd  8371  subdi  8372  mulneg2  8383  mulsub  8388  ltleadd  8433  ltsubpos  8441  posdif  8442  addge01  8459  lesub0  8466  reapneg  8584  prodgt02  8840  prodge02  8842  ltdivmul  8863  lerec  8871  lediv2a  8882  le2msq  8888  msq11  8889  lbreu  8932  dfinfre  8943  creur  8946  creui  8947  cju  8948  nnmulcl  8970  nndivtr  8991  avgle1  9189  avgle2  9190  nn0nnaddcl  9237  zletric  9327  zrevaddcl  9333  znnsub  9334  znn0sub  9348  ltsubnn0  9350  zdclt  9360  zextlt  9375  gtndiv  9378  prime  9382  peano5uzti  9391  uztrn2  9575  uztric  9579  uz11  9580  nn0pzuz  9617  indstr  9623  supinfneg  9625  infsupneg  9626  eluzdc  9640  qrevaddcl  9674  difrp  9722  xrltnsym  9823  xrltso  9826  xrlttri3  9827  xrletri3  9834  xleneg  9867  xaddcom  9891  xposdif  9912  ixxssixx  9932  iccid  9955  iooshf  9982  iccsupr  9996  iooneg  10018  iccneg  10019  fztri3or  10069  fzdcel  10070  fzn  10072  fzen  10073  fzass4  10092  fzrev  10114  fznn  10119  elfzp1b  10127  elfzm1b  10128  fz0fzdiffz0  10160  difelfznle  10165  fzon  10196  fzonmapblen  10217  eluzgtdifelfzo  10227  ubmelm1fzo  10256  subfzo0  10272  qletric  10274  ioo0  10290  ico0  10292  ioc0  10293  flqbi  10321  flqbi2  10322  flqzadd  10329  modfzo0difsn  10426  fzfig  10461  expcllem  10562  expap0  10581  mulbinom2  10668  expnbnd  10675  sq11ap  10719  hashfacen  10848  shftlem  10857  shftuz  10858  shftfvalg  10859  ovshftex  10860  shftfval  10862  shftval4  10869  shftval5  10870  2shfti  10872  mulreap  10905  sqrt11ap  11079  abs3dif  11146  abs2difabs  11149  maxabslemval  11249  maxle2  11253  maxclpr  11263  2zsupmax  11266  mingeb  11282  2zinfmin  11283  xrmaxiflemval  11290  xrmax2sup  11294  iooinsup  11317  climshftlemg  11342  fsumcnv  11477  explecnv  11545  geo2lim  11556  prodmodc  11618  fprodcnv  11665  demoivre  11812  demoivreALT  11813  nndivides  11836  0dvds  11850  muldvds1  11855  muldvds2  11856  dvdssubr  11878  dvdsadd2b  11879  odd2np1  11910  mulsucdiv2z  11922  ltoddhalfle  11930  ndvdssub  11967  gcdcom  12006  neggcd  12016  gcdabs2  12023  modgcd  12024  bezoutlemaz  12036  dfgcd2  12047  lcmcom  12096  neglcm  12107  lcmgcdeq  12115  coprmdvds  12124  qredeq  12128  divgcdcoprmex  12134  isprm3  12150  prmind2  12152  dvdsprm  12169  cncongrprm  12189  sqrt2irr  12194  hashgcdeq  12271  modprmn0modprm0  12288  coprimeprodsq  12289  pythagtriplem1  12297  pythagtriplem4  12300  pc2dvds  12362  pc11  12363  pcz  12364  pcprod  12378  prmunb  12394  1arithlem2  12396  1arithlem3  12397  1arith  12399  ptex  12769  issubmnd  12903  submcl  12931  resmhm2b  12941  grpinvsub  13026  dfgrp3mlem  13042  imasabl  13273  mgpress  13285  srgmulgass  13343  dfrhm2  13504  isrim0  13511  rmodislmodlem  13666  rmodislmod  13667  cnfldexp  13880  dvdsrzring  13902  eltg  14009  eltg2  14010  tgss  14020  tgss2  14036  basgen2  14038  bastop1  14040  opnneiss  14115  cnrest  14192  txss12  14223  hmeofvalg  14260  txswaphmeolem  14277  txswaphmeo  14278  blpnfctr  14396  metequiv  14452  metcnp3  14468  qtopbasss  14478  reopnap  14495  bl2ioo  14499  ioo2bl  14500  ioo2blex  14501  cncfval  14516  divccncfap  14534  addccncf  14543  expcncf  14549  dvexp  14632  dvef  14645  efle  14654  reapef  14656  ptolemy  14702  logleb  14753  lgsprme0  14901  2lgsoddprmlem2  14912  uzdcinzz  15008  exmidsbthrlem  15229  triap  15236