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  1291  mp3anr1  1334  mp3anr2  1335  mp3anr3  1336  eu5  2071  2exeu  2116  eqeqan12rd  2192  sylan9eqr  2230  r19.29vva  2620  morex  2919  sylan9ssr  3167  riinm  3954  breqan12rd  4015  elnn  4599  soinxp  4690  seinxp  4691  brelrng  4851  dminss  5035  imainss  5036  funsng  5254  funcnvuni  5277  f1co  5425  f1ocnv  5466  fun11iun  5474  funimass4  5558  fndmdifcom  5614  fsn2  5682  fvtp2g  5717  fvtp3g  5718  fvtp2  5720  fvtp3  5721  acexmid  5864  oveqan12rd  5885  cofunex2g  6101  brtposg  6245  tposoprab  6271  smores3  6284  smores2  6285  smoel  6291  tfri3  6358  rdgtfr  6365  rdgruledefgg  6366  omcl  6452  oeicl  6453  nnmsucr  6479  nnmcom  6480  nndir  6481  nnaordi  6499  nnaordr  6501  nnaword  6502  nnmordi  6507  nnaordex  6519  nnm00  6521  ersym  6537  elecg  6563  riinerm  6598  ecopovsym  6621  ecopovsymg  6624  ecovcom  6632  ecovicom  6633  mapvalg  6648  pmvalg  6649  elpmg  6654  elmapssres  6663  pmss12g  6665  ixpconstg  6697  ener  6769  domtr  6775  f1imaeng  6782  fundmen  6796  xpcomco  6816  xpsnen2g  6819  xpdom2  6821  xpdom1g  6823  enen2  6831  domen2  6833  ssfilem  6865  diffitest  6877  fiintim  6918  fundmfibi  6928  cnvti  7008  djuex  7032  nnnninf  7114  ltsopi  7294  pitric  7295  pitri3or  7296  addcompig  7303  mulcompig  7305  ltapig  7312  ltmpig  7313  nnppipi  7317  addcomnqg  7355  addassnqg  7356  distrnqg  7361  recexnq  7364  nqtri3or  7370  ltmnqg  7375  lt2addnq  7378  lt2mulnq  7379  ltbtwnnqq  7389  prarloclemarch2  7393  enq0ref  7407  distrnq0  7433  mulcomnq0  7434  prcdnql  7458  prcunqu  7459  prarloclemlt  7467  genpassl  7498  genpassu  7499  nqprloc  7519  nqpru  7526  appdiv0nq  7538  addcomprg  7552  mulcomprg  7554  distrlem4prl  7558  distrlem4pru  7559  1idprl  7564  1idpru  7565  ltsopr  7570  recexprlemss1l  7609  recexprlemss1u  7610  gt0srpr  7722  mulcomsrg  7731  ltsosr  7738  aptisr  7753  mulextsr1  7755  map2psrprg  7779  axaddcom  7844  axltwlin  7999  axapti  8002  letri3  8012  eqlelt  8018  mul31  8062  cnegexlem3  8108  subval  8123  subcl  8130  pncan2  8138  pncan3  8139  npcan  8140  addsubeq4  8146  npncan3  8169  negsubdi2  8190  muladd  8315  subdi  8316  mulneg2  8327  mulsub  8332  ltleadd  8377  ltsubpos  8385  posdif  8386  addge01  8403  lesub0  8410  reapneg  8528  prodgt02  8783  prodge02  8785  ltdivmul  8806  lerec  8814  lediv2a  8825  le2msq  8831  msq11  8832  lbreu  8875  dfinfre  8886  creur  8889  creui  8890  cju  8891  nnmulcl  8913  nndivtr  8934  avgle1  9132  avgle2  9133  nn0nnaddcl  9180  zletric  9270  zrevaddcl  9276  znnsub  9277  znn0sub  9291  ltsubnn0  9293  zdclt  9303  zextlt  9318  gtndiv  9321  prime  9325  peano5uzti  9334  uztrn2  9518  uztric  9522  uz11  9523  nn0pzuz  9560  indstr  9566  supinfneg  9568  infsupneg  9569  eluzdc  9583  qrevaddcl  9617  difrp  9663  xrltnsym  9764  xrltso  9767  xrlttri3  9768  xrletri3  9775  xleneg  9808  xaddcom  9832  xposdif  9853  ixxssixx  9873  iccid  9896  iooshf  9923  iccsupr  9937  iooneg  9959  iccneg  9960  fztri3or  10009  fzdcel  10010  fzn  10012  fzen  10013  fzass4  10032  fzrev  10054  fznn  10059  elfzp1b  10067  elfzm1b  10068  fz0fzdiffz0  10100  difelfznle  10105  fzon  10136  fzonmapblen  10157  eluzgtdifelfzo  10167  ubmelm1fzo  10196  subfzo0  10212  qletric  10214  ioo0  10230  ico0  10232  ioc0  10233  flqbi  10260  flqbi2  10261  flqzadd  10268  modfzo0difsn  10365  fzfig  10400  expcllem  10501  expap0  10520  mulbinom2  10606  expnbnd  10613  sq11ap  10657  hashfacen  10784  shftlem  10793  shftuz  10794  shftfvalg  10795  ovshftex  10796  shftfval  10798  shftval4  10805  shftval5  10806  2shfti  10808  mulreap  10841  sqrt11ap  11015  abs3dif  11082  abs2difabs  11085  maxabslemval  11185  maxle2  11189  maxclpr  11199  2zsupmax  11202  mingeb  11218  2zinfmin  11219  xrmaxiflemval  11226  xrmax2sup  11230  iooinsup  11253  climshftlemg  11278  fsumcnv  11413  explecnv  11481  geo2lim  11492  prodmodc  11554  fprodcnv  11601  demoivre  11748  demoivreALT  11749  nndivides  11772  0dvds  11786  muldvds1  11791  muldvds2  11792  dvdssubr  11814  dvdsadd2b  11815  odd2np1  11845  mulsucdiv2z  11857  ltoddhalfle  11865  ndvdssub  11902  gcdcom  11941  neggcd  11951  gcdabs2  11958  modgcd  11959  bezoutlemaz  11971  dfgcd2  11982  lcmcom  12031  neglcm  12042  lcmgcdeq  12050  coprmdvds  12059  qredeq  12063  divgcdcoprmex  12069  isprm3  12085  prmind2  12087  dvdsprm  12104  cncongrprm  12124  sqrt2irr  12129  hashgcdeq  12206  modprmn0modprm0  12223  coprimeprodsq  12224  pythagtriplem1  12232  pythagtriplem4  12235  pc2dvds  12296  pc11  12297  pcz  12298  pcprod  12311  prmunb  12327  1arithlem2  12329  1arithlem3  12330  1arith  12332  submcl  12741  grpinvsub  12822  dfgrp3mlem  12838  srgmulgass  12978  eltg  13132  eltg2  13133  tgss  13143  tgss2  13159  basgen2  13161  bastop1  13163  opnneiss  13238  cnrest  13315  txss12  13346  hmeofvalg  13383  txswaphmeolem  13400  txswaphmeo  13401  blpnfctr  13519  metequiv  13575  metcnp3  13591  qtopbasss  13601  reopnap  13618  bl2ioo  13622  ioo2bl  13623  ioo2blex  13624  cncfval  13639  divccncfap  13657  addccncf  13666  expcncf  13672  dvexp  13755  dvef  13768  efle  13777  reapef  13779  ptolemy  13825  logleb  13876  lgsprme0  14023  uzdcinzz  14119  exmidsbthrlem  14340  triap  14347