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  4698  soinxp  4789  seinxp  4790  brelrng  4955  dminss  5143  imainss  5144  funsng  5367  funcnvuni  5390  f1co  5545  f1ocnv  5587  fun11iun  5595  funimass4  5686  fndmdifcom  5743  fsn2  5811  fvtp2g  5852  fvtp3g  5853  fvtp2  5855  fvtp3  5856  riotaeqimp  5985  acexmid  6006  oveqan12rd  6027  cofunex2g  6261  brtposg  6406  tposoprab  6432  smores3  6445  smores2  6446  smoel  6452  tfri3  6519  rdgtfr  6526  rdgruledefgg  6527  omcl  6615  oeicl  6616  nnmsucr  6642  nnmcom  6643  nndir  6644  nnaordi  6662  nnaordr  6664  nnaword  6665  nnmordi  6670  nnaordex  6682  nnm00  6684  ersym  6700  elecg  6728  riinerm  6763  ecopovsym  6786  ecopovsymg  6789  ecovcom  6797  ecovicom  6798  mapvalg  6813  pmvalg  6814  elpmg  6819  elmapssres  6828  pmss12g  6830  ixpconstg  6862  domssr  6937  ener  6939  domtr  6945  f1imaeng  6952  fundmen  6967  xpcomco  6993  xpsnen2g  6996  xpdom2  6998  xpdom1g  7000  enen2  7010  domen2  7012  ssfilem  7045  diffitest  7057  fiintim  7101  fundmfibi  7113  cnvti  7194  djuex  7218  nnnninf  7301  netap  7448  2omotaplemap  7451  ltsopi  7515  pitric  7516  pitri3or  7517  addcompig  7524  mulcompig  7526  ltapig  7533  ltmpig  7534  nnppipi  7538  addcomnqg  7576  addassnqg  7577  distrnqg  7582  recexnq  7585  nqtri3or  7591  ltmnqg  7596  lt2addnq  7599  lt2mulnq  7600  ltbtwnnqq  7610  prarloclemarch2  7614  enq0ref  7628  distrnq0  7654  mulcomnq0  7655  prcdnql  7679  prcunqu  7680  prarloclemlt  7688  genpassl  7719  genpassu  7720  nqprloc  7740  nqpru  7747  appdiv0nq  7759  addcomprg  7773  mulcomprg  7775  distrlem4prl  7779  distrlem4pru  7780  1idprl  7785  1idpru  7786  ltsopr  7791  recexprlemss1l  7830  recexprlemss1u  7831  gt0srpr  7943  mulcomsrg  7952  ltsosr  7959  aptisr  7974  mulextsr1  7976  map2psrprg  8000  axaddcom  8065  axltwlin  8222  axapti  8225  letri3  8235  eqlelt  8241  mul31  8285  cnegexlem3  8331  subval  8346  subcl  8353  pncan2  8361  pncan3  8362  npcan  8363  addsubeq4  8369  npncan3  8392  negsubdi2  8413  muladd  8538  subdi  8539  mulneg2  8550  mulsub  8555  ltleadd  8601  ltsubpos  8609  posdif  8610  addge01  8627  lesub0  8634  reapneg  8752  prodgt02  9008  prodge02  9010  ltdivmul  9031  lerec  9039  lediv2a  9050  le2msq  9056  msq11  9057  lbreu  9100  dfinfre  9111  creur  9114  creui  9115  cju  9116  nnmulcl  9139  nndivtr  9160  avgle1  9360  avgle2  9361  nn0nnaddcl  9408  zletric  9498  zrevaddcl  9505  znnsub  9506  znn0sub  9520  ltsubnn0  9522  zdclt  9532  zextlt  9547  gtndiv  9550  prime  9554  peano5uzti  9563  uztrn2  9748  uztric  9752  uz11  9753  nn0pzuz  9790  indstr  9796  supinfneg  9798  infsupneg  9799  eluzdc  9813  qrevaddcl  9847  difrp  9896  xrltnsym  9997  xrltso  10000  xrlttri3  10001  xrletri3  10008  xleneg  10041  xaddcom  10065  xposdif  10086  ixxssixx  10106  iccid  10129  iooshf  10156  iccsupr  10170  iooneg  10192  iccneg  10193  fztri3or  10243  fzdcel  10244  fzn  10246  fzen  10247  fzass4  10266  fzrev  10288  fznn  10293  elfzp1b  10301  elfzm1b  10302  fz0fzdiffz0  10334  difelfznle  10339  fzon  10371  fzo0n  10372  fzonmapblen  10395  elfzoextl  10405  eluzgtdifelfzo  10411  ubmelm1fzo  10440  subfzo0  10456  qletric  10469  qdclt  10473  qdcle  10474  ioo0  10487  ico0  10489  ioc0  10490  flqbi  10518  flqbi2  10519  flqzadd  10526  modfzo0difsn  10625  fzfig  10660  expcllem  10780  expap0  10799  mulbinom2  10886  expnbnd  10893  sq11ap  10937  hashfacen  11066  iswrdinn0  11084  ccatsymb  11145  swrd0g  11200  swrdsbslen  11206  swrdspsleq  11207  wrd2ind  11263  pfxccatin12lem1  11268  pfxccatin12lem2  11271  pfxccatin12  11273  swrdccat3blem  11279  shftlem  11335  shftuz  11336  shftfvalg  11337  ovshftex  11338  shftfval  11340  shftval4  11347  shftval5  11348  2shfti  11350  mulreap  11383  sqrt11ap  11557  abs3dif  11624  abs2difabs  11627  maxabslemval  11727  maxle2  11731  maxclpr  11741  2zsupmax  11745  mingeb  11761  2zinfmin  11762  xrmaxiflemval  11769  xrmax2sup  11773  iooinsup  11796  climshftlemg  11821  fsumcnv  11956  explecnv  12024  geo2lim  12035  prodmodc  12097  fprodcnv  12144  demoivre  12292  demoivreALT  12293  nndivides  12316  0dvds  12330  muldvds1  12335  muldvds2  12336  dvdssubr  12358  dvdsadd2b  12359  odd2np1  12392  mulsucdiv2z  12404  ltoddhalfle  12412  ndvdssub  12449  gcdcom  12502  neggcd  12512  gcdabs2  12519  modgcd  12520  bezoutlemaz  12532  dfgcd2  12543  lcmcom  12594  neglcm  12605  lcmgcdeq  12613  coprmdvds  12622  qredeq  12626  divgcdcoprmex  12632  isprm3  12648  prmind2  12650  dvdsprm  12667  cncongrprm  12687  sqrt2irr  12692  hashgcdeq  12770  modprmn0modprm0  12787  coprimeprodsq  12788  pythagtriplem1  12796  pythagtriplem4  12799  pc2dvds  12861  pc11  12862  pcz  12863  pcprod  12877  prmunb  12893  1arithlem2  12895  1arithlem3  12896  1arith  12898  ptex  13305  issubmnd  13483  submcl  13520  resmhm2b  13530  grpinvsub  13623  dfgrp3mlem  13639  imasabl  13881  mgpress  13902  srgmulgass  13960  dfrhm2  14126  isrim0  14133  rmodislmodlem  14322  rmodislmod  14323  cnfldexp  14549  dvdsrzring  14575  znf1o  14623  eltg  14734  eltg2  14735  tgss  14745  tgss2  14761  basgen2  14763  bastop1  14765  opnneiss  14840  cnrest  14917  txss12  14948  hmeofvalg  14985  txswaphmeolem  15002  txswaphmeo  15003  blpnfctr  15121  metequiv  15177  metcnp3  15193  qtopbasss  15203  reopnap  15228  bl2ioo  15232  ioo2bl  15233  ioo2blex  15234  cncfval  15254  divccncfap  15272  addccncf  15282  expcncf  15291  dvexp  15393  dvmptfsum  15407  dvef  15409  efle  15458  reapef  15460  ptolemy  15506  logleb  15557  lgsprme0  15729  gausslemma2dlem1a  15745  gausslemma2dlem4  15751  lgsquadlem3  15766  2lgsoddprmlem2  15793  upgrpredgv  15952  uhgr2edg  16012  upgriswlkdc  16081  upgrwlkvtxedg  16085  g0wlk0  16091  uzdcinzz  16186  exmidsbthrlem  16420  triap  16427