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  601  bi2anan9r  609  syl3anr2  1324  mp3anr1  1368  mp3anr2  1369  mp3anr3  1370  stoic1b  1470  cbvaldvaw  1977  eu5  2125  2exeu  2170  eqeqan12rd  2246  sylan9eqr  2284  r19.29vva  2676  morex  2987  sylan9ssr  3238  riinm  4038  breqan12rd  4100  elnn  4699  soinxp  4791  seinxp  4792  brelrng  4958  dminss  5146  imainss  5147  funsng  5370  funcnvuni  5393  f1co  5548  f1ocnv  5590  fun11iun  5598  funimass4  5689  fndmdifcom  5746  fsn2  5814  fvtp2g  5855  fvtp3g  5856  fvtp2  5858  fvtp3  5859  riotaeqimp  5988  acexmid  6009  oveqan12rd  6030  cofunex2g  6264  brtposg  6411  tposoprab  6437  smores3  6450  smores2  6451  smoel  6457  tfri3  6524  rdgtfr  6531  rdgruledefgg  6532  omcl  6620  oeicl  6621  nnmsucr  6647  nnmcom  6648  nndir  6649  nnaordi  6667  nnaordr  6669  nnaword  6670  nnmordi  6675  nnaordex  6687  nnm00  6689  ersym  6705  elecg  6733  riinerm  6768  ecopovsym  6791  ecopovsymg  6794  ecovcom  6802  ecovicom  6803  mapvalg  6818  pmvalg  6819  elpmg  6824  elmapssres  6833  pmss12g  6835  ixpconstg  6867  domssr  6942  ener  6944  domtr  6950  f1imaeng  6957  fundmen  6972  xpcomco  6998  xpsnen2g  7001  xpdom2  7003  xpdom1g  7005  enen2  7015  domen2  7017  ssfilem  7050  diffitest  7062  fiintim  7109  fundmfibi  7121  cnvti  7202  djuex  7226  nnnninf  7309  netap  7456  2omotaplemap  7459  ltsopi  7523  pitric  7524  pitri3or  7525  addcompig  7532  mulcompig  7534  ltapig  7541  ltmpig  7542  nnppipi  7546  addcomnqg  7584  addassnqg  7585  distrnqg  7590  recexnq  7593  nqtri3or  7599  ltmnqg  7604  lt2addnq  7607  lt2mulnq  7608  ltbtwnnqq  7618  prarloclemarch2  7622  enq0ref  7636  distrnq0  7662  mulcomnq0  7663  prcdnql  7687  prcunqu  7688  prarloclemlt  7696  genpassl  7727  genpassu  7728  nqprloc  7748  nqpru  7755  appdiv0nq  7767  addcomprg  7781  mulcomprg  7783  distrlem4prl  7787  distrlem4pru  7788  1idprl  7793  1idpru  7794  ltsopr  7799  recexprlemss1l  7838  recexprlemss1u  7839  gt0srpr  7951  mulcomsrg  7960  ltsosr  7967  aptisr  7982  mulextsr1  7984  map2psrprg  8008  axaddcom  8073  axltwlin  8230  axapti  8233  letri3  8243  eqlelt  8249  mul31  8293  cnegexlem3  8339  subval  8354  subcl  8361  pncan2  8369  pncan3  8370  npcan  8371  addsubeq4  8377  npncan3  8400  negsubdi2  8421  muladd  8546  subdi  8547  mulneg2  8558  mulsub  8563  ltleadd  8609  ltsubpos  8617  posdif  8618  addge01  8635  lesub0  8642  reapneg  8760  prodgt02  9016  prodge02  9018  ltdivmul  9039  lerec  9047  lediv2a  9058  le2msq  9064  msq11  9065  lbreu  9108  dfinfre  9119  creur  9122  creui  9123  cju  9124  nnmulcl  9147  nndivtr  9168  avgle1  9368  avgle2  9369  nn0nnaddcl  9416  zletric  9506  zrevaddcl  9513  znnsub  9514  znn0sub  9528  ltsubnn0  9530  zdclt  9540  zextlt  9555  gtndiv  9558  prime  9562  peano5uzti  9571  uztrn2  9757  uztric  9761  uz11  9762  nn0pzuz  9799  indstr  9805  supinfneg  9807  infsupneg  9808  eluzdc  9822  qrevaddcl  9856  difrp  9905  xrltnsym  10006  xrltso  10009  xrlttri3  10010  xrletri3  10017  xleneg  10050  xaddcom  10074  xposdif  10095  ixxssixx  10115  iccid  10138  iooshf  10165  iccsupr  10179  iooneg  10201  iccneg  10202  fztri3or  10252  fzdcel  10253  fzn  10255  fzen  10256  fzass4  10275  fzrev  10297  fznn  10302  elfzp1b  10310  elfzm1b  10311  fz0fzdiffz0  10343  difelfznle  10348  fzon  10380  fzo0n  10381  fzonmapblen  10404  elfzoextl  10414  eluzgtdifelfzo  10420  ubmelm1fzo  10449  subfzo0  10465  qletric  10478  qdclt  10482  qdcle  10483  ioo0  10496  ico0  10498  ioc0  10499  flqbi  10527  flqbi2  10528  flqzadd  10535  modfzo0difsn  10634  fzfig  10669  expcllem  10789  expap0  10808  mulbinom2  10895  expnbnd  10902  sq11ap  10946  hashfacen  11076  iswrdinn0  11094  ccatsymb  11155  ccatalpha  11166  swrd0g  11213  swrdsbslen  11219  swrdspsleq  11220  wrd2ind  11276  pfxccatin12lem1  11281  pfxccatin12lem2  11284  pfxccatin12  11286  swrdccat3blem  11292  shftlem  11348  shftuz  11349  shftfvalg  11350  ovshftex  11351  shftfval  11353  shftval4  11360  shftval5  11361  2shfti  11363  mulreap  11396  sqrt11ap  11570  abs3dif  11637  abs2difabs  11640  maxabslemval  11740  maxle2  11744  maxclpr  11754  2zsupmax  11758  mingeb  11774  2zinfmin  11775  xrmaxiflemval  11782  xrmax2sup  11786  iooinsup  11809  climshftlemg  11834  fsumcnv  11969  explecnv  12037  geo2lim  12048  prodmodc  12110  fprodcnv  12157  demoivre  12305  demoivreALT  12306  nndivides  12329  0dvds  12343  muldvds1  12348  muldvds2  12349  dvdssubr  12371  dvdsadd2b  12372  odd2np1  12405  mulsucdiv2z  12417  ltoddhalfle  12425  ndvdssub  12462  gcdcom  12515  neggcd  12525  gcdabs2  12532  modgcd  12533  bezoutlemaz  12545  dfgcd2  12556  lcmcom  12607  neglcm  12618  lcmgcdeq  12626  coprmdvds  12635  qredeq  12639  divgcdcoprmex  12645  isprm3  12661  prmind2  12663  dvdsprm  12680  cncongrprm  12700  sqrt2irr  12705  hashgcdeq  12783  modprmn0modprm0  12800  coprimeprodsq  12801  pythagtriplem1  12809  pythagtriplem4  12812  pc2dvds  12874  pc11  12875  pcz  12876  pcprod  12890  prmunb  12906  1arithlem2  12908  1arithlem3  12909  1arith  12911  ptex  13318  issubmnd  13496  submcl  13533  resmhm2b  13543  grpinvsub  13636  dfgrp3mlem  13652  imasabl  13894  mgpress  13915  srgmulgass  13973  dfrhm2  14139  isrim0  14146  rmodislmodlem  14335  rmodislmod  14336  cnfldexp  14562  dvdsrzring  14588  znf1o  14636  eltg  14747  eltg2  14748  tgss  14758  tgss2  14774  basgen2  14776  bastop1  14778  opnneiss  14853  cnrest  14930  txss12  14961  hmeofvalg  14998  txswaphmeolem  15015  txswaphmeo  15016  blpnfctr  15134  metequiv  15190  metcnp3  15206  qtopbasss  15216  reopnap  15241  bl2ioo  15245  ioo2bl  15246  ioo2blex  15247  cncfval  15267  divccncfap  15285  addccncf  15295  expcncf  15304  dvexp  15406  dvmptfsum  15420  dvef  15422  efle  15471  reapef  15473  ptolemy  15519  logleb  15570  lgsprme0  15742  gausslemma2dlem1a  15758  gausslemma2dlem4  15764  lgsquadlem3  15779  2lgsoddprmlem2  15806  upgrpredgv  15965  uhgr2edg  16025  upgriswlkdc  16132  upgrwlkvtxedg  16136  g0wlk0  16142  clwwlkn1  16186  uzdcinzz  16271  exmidsbthrlem  16504  triap  16511