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  1945  eu5  2092  2exeu  2137  eqeqan12rd  2213  sylan9eqr  2251  r19.29vva  2642  morex  2948  sylan9ssr  3198  riinm  3990  breqan12rd  4051  elnn  4643  soinxp  4734  seinxp  4735  brelrng  4898  dminss  5085  imainss  5086  funsng  5305  funcnvuni  5328  f1co  5478  f1ocnv  5520  fun11iun  5528  funimass4  5614  fndmdifcom  5671  fsn2  5739  fvtp2g  5774  fvtp3g  5775  fvtp2  5777  fvtp3  5778  acexmid  5924  oveqan12rd  5945  cofunex2g  6176  brtposg  6321  tposoprab  6347  smores3  6360  smores2  6361  smoel  6367  tfri3  6434  rdgtfr  6441  rdgruledefgg  6442  omcl  6528  oeicl  6529  nnmsucr  6555  nnmcom  6556  nndir  6557  nnaordi  6575  nnaordr  6577  nnaword  6578  nnmordi  6583  nnaordex  6595  nnm00  6597  ersym  6613  elecg  6641  riinerm  6676  ecopovsym  6699  ecopovsymg  6702  ecovcom  6710  ecovicom  6711  mapvalg  6726  pmvalg  6727  elpmg  6732  elmapssres  6741  pmss12g  6743  ixpconstg  6775  ener  6847  domtr  6853  f1imaeng  6860  fundmen  6874  xpcomco  6894  xpsnen2g  6897  xpdom2  6899  xpdom1g  6901  enen2  6911  domen2  6913  ssfilem  6945  diffitest  6957  fiintim  7001  fundmfibi  7013  cnvti  7094  djuex  7118  nnnninf  7201  netap  7339  2omotaplemap  7342  ltsopi  7406  pitric  7407  pitri3or  7408  addcompig  7415  mulcompig  7417  ltapig  7424  ltmpig  7425  nnppipi  7429  addcomnqg  7467  addassnqg  7468  distrnqg  7473  recexnq  7476  nqtri3or  7482  ltmnqg  7487  lt2addnq  7490  lt2mulnq  7491  ltbtwnnqq  7501  prarloclemarch2  7505  enq0ref  7519  distrnq0  7545  mulcomnq0  7546  prcdnql  7570  prcunqu  7571  prarloclemlt  7579  genpassl  7610  genpassu  7611  nqprloc  7631  nqpru  7638  appdiv0nq  7650  addcomprg  7664  mulcomprg  7666  distrlem4prl  7670  distrlem4pru  7671  1idprl  7676  1idpru  7677  ltsopr  7682  recexprlemss1l  7721  recexprlemss1u  7722  gt0srpr  7834  mulcomsrg  7843  ltsosr  7850  aptisr  7865  mulextsr1  7867  map2psrprg  7891  axaddcom  7956  axltwlin  8113  axapti  8116  letri3  8126  eqlelt  8132  mul31  8176  cnegexlem3  8222  subval  8237  subcl  8244  pncan2  8252  pncan3  8253  npcan  8254  addsubeq4  8260  npncan3  8283  negsubdi2  8304  muladd  8429  subdi  8430  mulneg2  8441  mulsub  8446  ltleadd  8492  ltsubpos  8500  posdif  8501  addge01  8518  lesub0  8525  reapneg  8643  prodgt02  8899  prodge02  8901  ltdivmul  8922  lerec  8930  lediv2a  8941  le2msq  8947  msq11  8948  lbreu  8991  dfinfre  9002  creur  9005  creui  9006  cju  9007  nnmulcl  9030  nndivtr  9051  avgle1  9251  avgle2  9252  nn0nnaddcl  9299  zletric  9389  zrevaddcl  9395  znnsub  9396  znn0sub  9410  ltsubnn0  9412  zdclt  9422  zextlt  9437  gtndiv  9440  prime  9444  peano5uzti  9453  uztrn2  9638  uztric  9642  uz11  9643  nn0pzuz  9680  indstr  9686  supinfneg  9688  infsupneg  9689  eluzdc  9703  qrevaddcl  9737  difrp  9786  xrltnsym  9887  xrltso  9890  xrlttri3  9891  xrletri3  9898  xleneg  9931  xaddcom  9955  xposdif  9976  ixxssixx  9996  iccid  10019  iooshf  10046  iccsupr  10060  iooneg  10082  iccneg  10083  fztri3or  10133  fzdcel  10134  fzn  10136  fzen  10137  fzass4  10156  fzrev  10178  fznn  10183  elfzp1b  10191  elfzm1b  10192  fz0fzdiffz0  10224  difelfznle  10229  fzon  10261  fzonmapblen  10282  eluzgtdifelfzo  10292  ubmelm1fzo  10321  subfzo0  10337  qletric  10350  qdclt  10354  qdcle  10355  ioo0  10368  ico0  10370  ioc0  10371  flqbi  10399  flqbi2  10400  flqzadd  10407  modfzo0difsn  10506  fzfig  10541  expcllem  10661  expap0  10680  mulbinom2  10767  expnbnd  10774  sq11ap  10818  hashfacen  10947  iswrdinn0  10959  shftlem  11000  shftuz  11001  shftfvalg  11002  ovshftex  11003  shftfval  11005  shftval4  11012  shftval5  11013  2shfti  11015  mulreap  11048  sqrt11ap  11222  abs3dif  11289  abs2difabs  11292  maxabslemval  11392  maxle2  11396  maxclpr  11406  2zsupmax  11410  mingeb  11426  2zinfmin  11427  xrmaxiflemval  11434  xrmax2sup  11438  iooinsup  11461  climshftlemg  11486  fsumcnv  11621  explecnv  11689  geo2lim  11700  prodmodc  11762  fprodcnv  11809  demoivre  11957  demoivreALT  11958  nndivides  11981  0dvds  11995  muldvds1  12000  muldvds2  12001  dvdssubr  12023  dvdsadd2b  12024  odd2np1  12057  mulsucdiv2z  12069  ltoddhalfle  12077  ndvdssub  12114  gcdcom  12167  neggcd  12177  gcdabs2  12184  modgcd  12185  bezoutlemaz  12197  dfgcd2  12208  lcmcom  12259  neglcm  12270  lcmgcdeq  12278  coprmdvds  12287  qredeq  12291  divgcdcoprmex  12297  isprm3  12313  prmind2  12315  dvdsprm  12332  cncongrprm  12352  sqrt2irr  12357  hashgcdeq  12435  modprmn0modprm0  12452  coprimeprodsq  12453  pythagtriplem1  12461  pythagtriplem4  12464  pc2dvds  12526  pc11  12527  pcz  12528  pcprod  12542  prmunb  12558  1arithlem2  12560  1arithlem3  12561  1arith  12563  ptex  12968  issubmnd  13146  submcl  13183  resmhm2b  13193  grpinvsub  13286  dfgrp3mlem  13302  imasabl  13544  mgpress  13565  srgmulgass  13623  dfrhm2  13788  isrim0  13795  rmodislmodlem  13984  rmodislmod  13985  cnfldexp  14211  dvdsrzring  14237  znf1o  14285  eltg  14374  eltg2  14375  tgss  14385  tgss2  14401  basgen2  14403  bastop1  14405  opnneiss  14480  cnrest  14557  txss12  14588  hmeofvalg  14625  txswaphmeolem  14642  txswaphmeo  14643  blpnfctr  14761  metequiv  14817  metcnp3  14833  qtopbasss  14843  reopnap  14868  bl2ioo  14872  ioo2bl  14873  ioo2blex  14874  cncfval  14894  divccncfap  14912  addccncf  14922  expcncf  14931  dvexp  15033  dvmptfsum  15047  dvef  15049  efle  15098  reapef  15100  ptolemy  15146  logleb  15197  lgsprme0  15369  gausslemma2dlem1a  15385  gausslemma2dlem4  15391  lgsquadlem3  15406  2lgsoddprmlem2  15433  uzdcinzz  15530  exmidsbthrlem  15757  triap  15764