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  cbvaldvaw  1942  eu5  2089  2exeu  2134  eqeqan12rd  2210  sylan9eqr  2248  r19.29vva  2639  morex  2944  sylan9ssr  3193  riinm  3985  breqan12rd  4046  elnn  4638  soinxp  4729  seinxp  4730  brelrng  4893  dminss  5080  imainss  5081  funsng  5300  funcnvuni  5323  f1co  5471  f1ocnv  5513  fun11iun  5521  funimass4  5607  fndmdifcom  5664  fsn2  5732  fvtp2g  5767  fvtp3g  5768  fvtp2  5770  fvtp3  5771  acexmid  5917  oveqan12rd  5938  cofunex2g  6162  brtposg  6307  tposoprab  6333  smores3  6346  smores2  6347  smoel  6353  tfri3  6420  rdgtfr  6427  rdgruledefgg  6428  omcl  6514  oeicl  6515  nnmsucr  6541  nnmcom  6542  nndir  6543  nnaordi  6561  nnaordr  6563  nnaword  6564  nnmordi  6569  nnaordex  6581  nnm00  6583  ersym  6599  elecg  6627  riinerm  6662  ecopovsym  6685  ecopovsymg  6688  ecovcom  6696  ecovicom  6697  mapvalg  6712  pmvalg  6713  elpmg  6718  elmapssres  6727  pmss12g  6729  ixpconstg  6761  ener  6833  domtr  6839  f1imaeng  6846  fundmen  6860  xpcomco  6880  xpsnen2g  6883  xpdom2  6885  xpdom1g  6887  enen2  6897  domen2  6899  ssfilem  6931  diffitest  6943  fiintim  6985  fundmfibi  6997  cnvti  7078  djuex  7102  nnnninf  7185  netap  7314  2omotaplemap  7317  ltsopi  7380  pitric  7381  pitri3or  7382  addcompig  7389  mulcompig  7391  ltapig  7398  ltmpig  7399  nnppipi  7403  addcomnqg  7441  addassnqg  7442  distrnqg  7447  recexnq  7450  nqtri3or  7456  ltmnqg  7461  lt2addnq  7464  lt2mulnq  7465  ltbtwnnqq  7475  prarloclemarch2  7479  enq0ref  7493  distrnq0  7519  mulcomnq0  7520  prcdnql  7544  prcunqu  7545  prarloclemlt  7553  genpassl  7584  genpassu  7585  nqprloc  7605  nqpru  7612  appdiv0nq  7624  addcomprg  7638  mulcomprg  7640  distrlem4prl  7644  distrlem4pru  7645  1idprl  7650  1idpru  7651  ltsopr  7656  recexprlemss1l  7695  recexprlemss1u  7696  gt0srpr  7808  mulcomsrg  7817  ltsosr  7824  aptisr  7839  mulextsr1  7841  map2psrprg  7865  axaddcom  7930  axltwlin  8087  axapti  8090  letri3  8100  eqlelt  8106  mul31  8150  cnegexlem3  8196  subval  8211  subcl  8218  pncan2  8226  pncan3  8227  npcan  8228  addsubeq4  8234  npncan3  8257  negsubdi2  8278  muladd  8403  subdi  8404  mulneg2  8415  mulsub  8420  ltleadd  8465  ltsubpos  8473  posdif  8474  addge01  8491  lesub0  8498  reapneg  8616  prodgt02  8872  prodge02  8874  ltdivmul  8895  lerec  8903  lediv2a  8914  le2msq  8920  msq11  8921  lbreu  8964  dfinfre  8975  creur  8978  creui  8979  cju  8980  nnmulcl  9003  nndivtr  9024  avgle1  9223  avgle2  9224  nn0nnaddcl  9271  zletric  9361  zrevaddcl  9367  znnsub  9368  znn0sub  9382  ltsubnn0  9384  zdclt  9394  zextlt  9409  gtndiv  9412  prime  9416  peano5uzti  9425  uztrn2  9610  uztric  9614  uz11  9615  nn0pzuz  9652  indstr  9658  supinfneg  9660  infsupneg  9661  eluzdc  9675  qrevaddcl  9709  difrp  9758  xrltnsym  9859  xrltso  9862  xrlttri3  9863  xrletri3  9870  xleneg  9903  xaddcom  9927  xposdif  9948  ixxssixx  9968  iccid  9991  iooshf  10018  iccsupr  10032  iooneg  10054  iccneg  10055  fztri3or  10105  fzdcel  10106  fzn  10108  fzen  10109  fzass4  10128  fzrev  10150  fznn  10155  elfzp1b  10163  elfzm1b  10164  fz0fzdiffz0  10196  difelfznle  10201  fzon  10233  fzonmapblen  10254  eluzgtdifelfzo  10264  ubmelm1fzo  10293  subfzo0  10309  qletric  10311  qdclt  10315  ioo0  10328  ico0  10330  ioc0  10331  flqbi  10359  flqbi2  10360  flqzadd  10367  modfzo0difsn  10466  fzfig  10501  expcllem  10621  expap0  10640  mulbinom2  10727  expnbnd  10734  sq11ap  10778  hashfacen  10907  iswrdinn0  10919  shftlem  10960  shftuz  10961  shftfvalg  10962  ovshftex  10963  shftfval  10965  shftval4  10972  shftval5  10973  2shfti  10975  mulreap  11008  sqrt11ap  11182  abs3dif  11249  abs2difabs  11252  maxabslemval  11352  maxle2  11356  maxclpr  11366  2zsupmax  11369  mingeb  11385  2zinfmin  11386  xrmaxiflemval  11393  xrmax2sup  11397  iooinsup  11420  climshftlemg  11445  fsumcnv  11580  explecnv  11648  geo2lim  11659  prodmodc  11721  fprodcnv  11768  demoivre  11916  demoivreALT  11917  nndivides  11940  0dvds  11954  muldvds1  11959  muldvds2  11960  dvdssubr  11982  dvdsadd2b  11983  odd2np1  12014  mulsucdiv2z  12026  ltoddhalfle  12034  ndvdssub  12071  gcdcom  12110  neggcd  12120  gcdabs2  12127  modgcd  12128  bezoutlemaz  12140  dfgcd2  12151  lcmcom  12202  neglcm  12213  lcmgcdeq  12221  coprmdvds  12230  qredeq  12234  divgcdcoprmex  12240  isprm3  12256  prmind2  12258  dvdsprm  12275  cncongrprm  12295  sqrt2irr  12300  hashgcdeq  12377  modprmn0modprm0  12394  coprimeprodsq  12395  pythagtriplem1  12403  pythagtriplem4  12406  pc2dvds  12468  pc11  12469  pcz  12470  pcprod  12484  prmunb  12500  1arithlem2  12502  1arithlem3  12503  1arith  12505  ptex  12875  issubmnd  13023  submcl  13051  resmhm2b  13061  grpinvsub  13154  dfgrp3mlem  13170  imasabl  13406  mgpress  13427  srgmulgass  13485  dfrhm2  13650  isrim0  13657  rmodislmodlem  13846  rmodislmod  13847  cnfldexp  14065  dvdsrzring  14091  znf1o  14139  eltg  14220  eltg2  14221  tgss  14231  tgss2  14247  basgen2  14249  bastop1  14251  opnneiss  14326  cnrest  14403  txss12  14434  hmeofvalg  14471  txswaphmeolem  14488  txswaphmeo  14489  blpnfctr  14607  metequiv  14663  metcnp3  14679  qtopbasss  14689  reopnap  14706  bl2ioo  14710  ioo2bl  14711  ioo2blex  14712  cncfval  14727  divccncfap  14745  addccncf  14754  expcncf  14763  dvexp  14860  dvef  14873  efle  14911  reapef  14913  ptolemy  14959  logleb  15010  lgsprme0  15158  gausslemma2dlem1a  15174  gausslemma2dlem4  15180  2lgsoddprmlem2  15194  uzdcinzz  15290  exmidsbthrlem  15512  triap  15519