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  2988  sylan9ssr  3239  riinm  4041  breqan12rd  4103  elnn  4702  soinxp  4794  seinxp  4795  brelrng  4961  dminss  5149  imainss  5150  funsng  5373  funcnvuni  5396  f1co  5551  f1ocnv  5593  fun11iun  5601  funimass4  5692  fndmdifcom  5749  fsn2  5817  fvtp2g  5858  fvtp3g  5859  fvtp2  5861  fvtp3  5862  riotaeqimp  5991  acexmid  6012  oveqan12rd  6033  cofunex2g  6267  brtposg  6415  tposoprab  6441  smores3  6454  smores2  6455  smoel  6461  tfri3  6528  rdgtfr  6535  rdgruledefgg  6536  omcl  6624  oeicl  6625  nnmsucr  6651  nnmcom  6652  nndir  6653  nnaordi  6671  nnaordr  6673  nnaword  6674  nnmordi  6679  nnaordex  6691  nnm00  6693  ersym  6709  elecg  6737  riinerm  6772  ecopovsym  6795  ecopovsymg  6798  ecovcom  6806  ecovicom  6807  mapvalg  6822  pmvalg  6823  elpmg  6828  elmapssres  6837  pmss12g  6839  ixpconstg  6871  domssr  6946  ener  6948  domtr  6954  f1imaeng  6961  fundmen  6976  xpcomco  7005  xpsnen2g  7008  xpdom2  7010  xpdom1g  7012  enen2  7022  domen2  7024  ssfilem  7057  ssfilemd  7059  diffitest  7071  fiintim  7118  fundmfibi  7131  cnvti  7212  djuex  7236  nnnninf  7319  netap  7466  2omotaplemap  7469  ltsopi  7533  pitric  7534  pitri3or  7535  addcompig  7542  mulcompig  7544  ltapig  7551  ltmpig  7552  nnppipi  7556  addcomnqg  7594  addassnqg  7595  distrnqg  7600  recexnq  7603  nqtri3or  7609  ltmnqg  7614  lt2addnq  7617  lt2mulnq  7618  ltbtwnnqq  7628  prarloclemarch2  7632  enq0ref  7646  distrnq0  7672  mulcomnq0  7673  prcdnql  7697  prcunqu  7698  prarloclemlt  7706  genpassl  7737  genpassu  7738  nqprloc  7758  nqpru  7765  appdiv0nq  7777  addcomprg  7791  mulcomprg  7793  distrlem4prl  7797  distrlem4pru  7798  1idprl  7803  1idpru  7804  ltsopr  7809  recexprlemss1l  7848  recexprlemss1u  7849  gt0srpr  7961  mulcomsrg  7970  ltsosr  7977  aptisr  7992  mulextsr1  7994  map2psrprg  8018  axaddcom  8083  axltwlin  8240  axapti  8243  letri3  8253  eqlelt  8259  mul31  8303  cnegexlem3  8349  subval  8364  subcl  8371  pncan2  8379  pncan3  8380  npcan  8381  addsubeq4  8387  npncan3  8410  negsubdi2  8431  muladd  8556  subdi  8557  mulneg2  8568  mulsub  8573  ltleadd  8619  ltsubpos  8627  posdif  8628  addge01  8645  lesub0  8652  reapneg  8770  prodgt02  9026  prodge02  9028  ltdivmul  9049  lerec  9057  lediv2a  9068  le2msq  9074  msq11  9075  lbreu  9118  dfinfre  9129  creur  9132  creui  9133  cju  9134  nnmulcl  9157  nndivtr  9178  avgle1  9378  avgle2  9379  nn0nnaddcl  9426  zletric  9516  zrevaddcl  9523  znnsub  9524  znn0sub  9538  ltsubnn0  9540  zdclt  9550  zextlt  9565  gtndiv  9568  prime  9572  peano5uzti  9581  uztrn2  9767  uztric  9771  uz11  9772  nn0pzuz  9814  indstr  9820  supinfneg  9822  infsupneg  9823  eluzdc  9837  qrevaddcl  9871  difrp  9920  xrltnsym  10021  xrltso  10024  xrlttri3  10025  xrletri3  10032  xleneg  10065  xaddcom  10089  xposdif  10110  ixxssixx  10130  iccid  10153  iooshf  10180  iccsupr  10194  iooneg  10216  iccneg  10217  fztri3or  10267  fzdcel  10268  fzn  10270  fzen  10271  fzass4  10290  fzrev  10312  fznn  10317  elfzp1b  10325  elfzm1b  10326  fz0fzdiffz0  10358  difelfznle  10363  fzon  10395  fzo0n  10396  fzonmapblen  10419  elfzoextl  10429  eluzgtdifelfzo  10435  ubmelm1fzo  10464  subfzo0  10481  qletric  10494  qdclt  10498  qdcle  10499  ioo0  10512  ico0  10514  ioc0  10515  flqbi  10543  flqbi2  10544  flqzadd  10551  modfzo0difsn  10650  fzfig  10685  expcllem  10805  expap0  10824  mulbinom2  10911  expnbnd  10918  sq11ap  10962  hashfacen  11093  iswrdinn0  11111  ccatsymb  11172  ccatalpha  11183  swrd0g  11234  swrdsbslen  11240  swrdspsleq  11241  wrd2ind  11297  pfxccatin12lem1  11302  pfxccatin12lem2  11305  pfxccatin12  11307  swrdccat3blem  11313  shftlem  11370  shftuz  11371  shftfvalg  11372  ovshftex  11373  shftfval  11375  shftval4  11382  shftval5  11383  2shfti  11385  mulreap  11418  sqrt11ap  11592  abs3dif  11659  abs2difabs  11662  maxabslemval  11762  maxle2  11766  maxclpr  11776  2zsupmax  11780  mingeb  11796  2zinfmin  11797  xrmaxiflemval  11804  xrmax2sup  11808  iooinsup  11831  climshftlemg  11856  fsumcnv  11991  explecnv  12059  geo2lim  12070  prodmodc  12132  fprodcnv  12179  demoivre  12327  demoivreALT  12328  nndivides  12351  0dvds  12365  muldvds1  12370  muldvds2  12371  dvdssubr  12393  dvdsadd2b  12394  odd2np1  12427  mulsucdiv2z  12439  ltoddhalfle  12447  ndvdssub  12484  gcdcom  12537  neggcd  12547  gcdabs2  12554  modgcd  12555  bezoutlemaz  12567  dfgcd2  12578  lcmcom  12629  neglcm  12640  lcmgcdeq  12648  coprmdvds  12657  qredeq  12661  divgcdcoprmex  12667  isprm3  12683  prmind2  12685  dvdsprm  12702  cncongrprm  12722  sqrt2irr  12727  hashgcdeq  12805  modprmn0modprm0  12822  coprimeprodsq  12823  pythagtriplem1  12831  pythagtriplem4  12834  pc2dvds  12896  pc11  12897  pcz  12898  pcprod  12912  prmunb  12928  1arithlem2  12930  1arithlem3  12931  1arith  12933  ptex  13340  issubmnd  13518  submcl  13555  resmhm2b  13565  grpinvsub  13658  dfgrp3mlem  13674  imasabl  13916  mgpress  13937  srgmulgass  13995  dfrhm2  14161  isrim0  14168  rmodislmodlem  14357  rmodislmod  14358  cnfldexp  14584  dvdsrzring  14610  znf1o  14658  eltg  14769  eltg2  14770  tgss  14780  tgss2  14796  basgen2  14798  bastop1  14800  opnneiss  14875  cnrest  14952  txss12  14983  hmeofvalg  15020  txswaphmeolem  15037  txswaphmeo  15038  blpnfctr  15156  metequiv  15212  metcnp3  15228  qtopbasss  15238  reopnap  15263  bl2ioo  15267  ioo2bl  15268  ioo2blex  15269  cncfval  15289  divccncfap  15307  addccncf  15317  expcncf  15326  dvexp  15428  dvmptfsum  15442  dvef  15444  efle  15493  reapef  15495  ptolemy  15541  logleb  15592  lgsprme0  15764  gausslemma2dlem1a  15780  gausslemma2dlem4  15786  lgsquadlem3  15801  2lgsoddprmlem2  15828  upgrpredgv  15990  uhgr2edg  16050  upgriswlkdc  16171  upgrwlkvtxedg  16175  g0wlk0  16181  clwwlkn1  16227  clwwlknonex2lem2  16247  uzdcinzz  16344  exmidsbthrlem  16576  triap  16583