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  579  anabsi7  583  anabsi8  584  im2anan9r  603  bi2anan9r  611  syl3anr2  1327  mp3anr1  1371  mp3anr2  1372  mp3anr3  1373  stoic1b  1473  cbvaldvaw  1982  eu5  2130  2exeu  2175  eqeqan12rd  2251  sylan9eqr  2289  r19.29vva  2690  morex  3004  sylan9ssr  3256  riinm  4069  breqan12rd  4131  elnn  4733  soinxp  4825  seinxp  4826  brelrng  4993  dminss  5182  imainss  5183  funsng  5407  funcnvuni  5430  f1co  5590  f1ocnv  5632  fun11iun  5640  funimass4  5732  fndmdifcom  5789  fsn2  5856  fvtp2g  5898  fvtp3g  5899  fvtp2  5901  fvtp3  5902  riotaeqimp  6036  acexmid  6057  oveqan12rd  6078  cofunex2g  6312  brtposg  6498  tposoprab  6524  smores3  6537  smores2  6538  smoel  6544  tfri3  6611  rdgtfr  6618  rdgruledefgg  6619  omcl  6707  oeicl  6708  nnmsucr  6734  nnmcom  6735  nndir  6736  nnaordi  6754  nnaordr  6756  nnaword  6757  nnmordi  6762  nnaordex  6774  nnm00  6776  ersym  6792  elecg  6820  riinerm  6855  ecopovsym  6878  ecopovsymg  6881  ecovcom  6889  ecovicom  6890  mapvalg  6905  pmvalg  6906  elpmg  6911  elmapssres  6920  pmss12g  6922  ixpconstg  6955  domssr  7030  ener  7032  domtr  7038  f1imaeng  7045  fundmen  7060  xpcomco  7090  xpsnen2g  7093  xpdom2  7095  xpdom1g  7097  enen2  7107  domen2  7109  ssfilem  7143  ssfilemd  7145  diffitest  7157  fiintim  7204  fundmfibi  7218  cnvti  7323  djuex  7347  nnnninf  7430  netap  7584  2omotaplemap  7587  ltsopi  7651  pitric  7652  pitri3or  7653  addcompig  7660  mulcompig  7662  ltapig  7669  ltmpig  7670  nnppipi  7674  addcomnqg  7712  addassnqg  7713  distrnqg  7718  recexnq  7721  nqtri3or  7727  ltmnqg  7732  lt2addnq  7735  lt2mulnq  7736  ltbtwnnqq  7746  prarloclemarch2  7750  enq0ref  7764  distrnq0  7790  mulcomnq0  7791  prcdnql  7815  prcunqu  7816  prarloclemlt  7824  genpassl  7855  genpassu  7856  nqprloc  7876  nqpru  7883  appdiv0nq  7895  addcomprg  7909  mulcomprg  7911  distrlem4prl  7915  distrlem4pru  7916  1idprl  7921  1idpru  7922  ltsopr  7927  recexprlemss1l  7966  recexprlemss1u  7967  gt0srpr  8079  mulcomsrg  8088  ltsosr  8095  aptisr  8110  mulextsr1  8112  map2psrprg  8136  axaddcom  8201  axltwlin  8357  axapti  8360  letri3  8370  eqlelt  8376  mul31  8421  cnegexlem3  8467  subval  8482  subcl  8489  pncan2  8497  pncan3  8498  npcan  8499  addsubeq4  8505  npncan3  8528  negsubdi2  8549  muladd  8675  subdi  8676  mulneg2  8687  mulsub  8692  ltleadd  8738  ltsubpos  8746  posdif  8747  addge01  8764  lesub0  8771  reapneg  8889  prodgt02  9147  prodge02  9149  ltdivmul  9170  lerec  9178  lediv2a  9189  le2msq  9195  msq11  9196  lbreu  9239  dfinfre  9250  creur  9253  creui  9254  cju  9255  nnmulcl  9278  nndivtr  9299  avgle1  9499  avgle2  9500  nn0nnaddcl  9547  zletric  9641  zrevaddcl  9648  znnsub  9649  znn0sub  9663  ltsubnn0  9665  zdclt  9675  zextlt  9691  gtndiv  9694  prime  9698  peano5uzti  9707  uztrn2  9893  uztric  9897  uz11  9898  nn0pzuz  9940  indstr  9946  supinfneg  9948  infsupneg  9949  eluzdc  9963  qrevaddcl  9997  difrp  10046  xrltnsym  10148  xrltso  10151  xrlttri3  10152  xrletri3  10159  xleneg  10192  xaddcom  10216  xposdif  10237  ixxssixx  10257  iccid  10280  iooshf  10307  iccsupr  10321  iooneg  10343  iccneg  10344  fztri3or  10396  fzdcel  10397  fzn  10399  fzen  10400  fzass4  10420  fzrev  10443  fznn  10448  elfzp1b  10456  elfzm1b  10457  fz0fzdiffz0  10489  difelfznle  10494  fzon  10526  fzo0n  10527  fzonmapblen  10551  elfzoextl  10561  eluzgtdifelfzo  10567  ubmelm1fzo  10596  subfzo0  10613  qletric  10628  qdclt  10632  qdcle  10633  ioo0  10646  ico0  10648  ioc0  10649  flqbi  10677  flqbi2  10678  flqzadd  10685  modfzo0difsn  10784  fzfig  10819  expcllem  10939  expap0  10958  mulbinom2  11045  expnbnd  11053  sq11ap  11097  hashfacen  11236  iswrdinn0  11257  ccatsymb  11318  ccatalpha  11329  swrd0g  11380  swrdsbslen  11386  swrdspsleq  11387  wrd2ind  11443  pfxccatin12lem1  11448  pfxccatin12lem2  11451  pfxccatin12  11453  swrdccat3blem  11459  shftlem  11529  shftuz  11530  shftfvalg  11531  ovshftex  11532  shftfval  11534  shftval4  11541  shftval5  11542  2shfti  11544  mulreap  11577  sqrt11ap  11752  abs3dif  11819  abs2difabs  11822  maxabslemval  11922  maxle2  11926  maxclpr  11936  2zsupmax  11940  mingeb  11956  2zinfmin  11957  xrmaxiflemval  11964  xrmax2sup  11968  iooinsup  11991  climshftlemg  12016  fsumcnv  12152  explecnv  12220  geo2lim  12231  prodmodc  12293  fprodcnv  12340  demoivre  12488  demoivreALT  12489  nndivides  12512  0dvds  12526  muldvds1  12531  muldvds2  12532  dvdssubr  12554  dvdsadd2b  12555  odd2np1  12588  mulsucdiv2z  12600  ltoddhalfle  12608  ndvdssub  12645  gcdcom  12698  neggcd  12708  gcdabs2  12715  modgcd  12716  bezoutlemaz  12728  dfgcd2  12739  lcmcom  12790  neglcm  12801  lcmgcdeq  12809  coprmdvds  12818  qredeq  12822  divgcdcoprmex  12828  isprm3  12844  prmind2  12846  dvdsprm  12863  cncongrprm  12883  sqrt2irr  12888  hashgcdeq  12966  modprmn0modprm0  12983  coprimeprodsq  12984  pythagtriplem1  12992  pythagtriplem4  12995  pc2dvds  13057  pc11  13058  pcz  13059  pcprod  13073  prmunb  13089  1arithlem2  13091  1arithlem3  13092  1arith  13094  ptex  13565  issubmnd  13707  submcl  13738  resmhm2b  13748  grpinvsub  13841  dfgrp3mlem  13857  imasabl  14093  mgpress  14174  srgmulgass  14236  dfrhm2  14403  isrim0  14410  rmodislmodlem  14628  rmodislmod  14629  cnfldexp  14855  dvdsrzring  14881  znf1o  14929  eltg  15047  eltg2  15048  tgss  15058  tgss2  15074  basgen2  15076  bastop1  15078  opnneiss  15153  cnrest  15230  txss12  15261  hmeofvalg  15298  txswaphmeolem  15315  txswaphmeo  15316  blpnfctr  15434  metequiv  15490  metcnp3  15506  qtopbasss  15516  reopnap  15541  bl2ioo  15545  ioo2bl  15546  ioo2blex  15547  cncfval  15567  divccncfap  15585  addccncf  15595  expcncf  15604  dvexp  15706  dvmptfsum  15720  dvef  15722  efle  15771  reapef  15773  ptolemy  15819  logleb  15870  lgsprme0  16045  gausslemma2dlem1a  16061  gausslemma2dlem4  16067  lgsquadlem3  16082  2lgsoddprmlem2  16109  upgrpredgv  16271  uhgr2edg  16331  issubgr  16382  subgrprop  16384  subuhgr  16397  subupgr  16398  subumgr  16399  subusgr  16400  upgriswlkdc  16485  upgrwlkvtxedg  16489  g0wlk0  16495  clwwlkn1  16543  clwwlknonex2lem2  16563  dichmul0orlem3  16639  uzdcinzz  16710  exmidsbthrlem  16942  triap  16953