Theorem ancoms 266

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 115	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 123	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  adantl  275  syl2anr  288  anim12ci  337  sylan9bbr  459  anabss4  567  anabsi7  571  anabsi8  572  im2anan9r  589  bi2anan9r  597  syl3anr2  1281  mp3anr1  1324  mp3anr2  1325  mp3anr3  1326  eu5  2061  2exeu  2106  eqeqan12rd  2182  sylan9eqr  2221  r19.29vva  2611  morex  2910  sylan9ssr  3156  riinm  3938  breqan12rd  3999  elnn  4583  soinxp  4674  seinxp  4675  brelrng  4835  dminss  5018  imainss  5019  funsng  5234  funcnvuni  5257  f1co  5405  f1ocnv  5445  fun11iun  5453  funimass4  5537  fndmdifcom  5591  fsn2  5659  fvtp2g  5694  fvtp3g  5695  fvtp2  5697  fvtp3  5698  acexmid  5841  oveqan12rd  5862  cofunex2g  6078  brtposg  6222  tposoprab  6248  smores3  6261  smores2  6262  smoel  6268  tfri3  6335  rdgtfr  6342  rdgruledefgg  6343  omcl  6429  oeicl  6430  nnmsucr  6456  nnmcom  6457  nndir  6458  nnaordi  6476  nnaordr  6478  nnaword  6479  nnmordi  6484  nnaordex  6495  nnm00  6497  ersym  6513  elecg  6539  riinerm  6574  ecopovsym  6597  ecopovsymg  6600  ecovcom  6608  ecovicom  6609  mapvalg  6624  pmvalg  6625  elpmg  6630  elmapssres  6639  pmss12g  6641  ixpconstg  6673  ener  6745  domtr  6751  f1imaeng  6758  fundmen  6772  xpcomco  6792  xpsnen2g  6795  xpdom2  6797  xpdom1g  6799  enen2  6807  domen2  6809  ssfilem  6841  diffitest  6853  fiintim  6894  fundmfibi  6904  cnvti  6984  djuex  7008  nnnninf  7090  ltsopi  7261  pitric  7262  pitri3or  7263  addcompig  7270  mulcompig  7272  ltapig  7279  ltmpig  7280  nnppipi  7284  addcomnqg  7322  addassnqg  7323  distrnqg  7328  recexnq  7331  nqtri3or  7337  ltmnqg  7342  lt2addnq  7345  lt2mulnq  7346  ltbtwnnqq  7356  prarloclemarch2  7360  enq0ref  7374  distrnq0  7400  mulcomnq0  7401  prcdnql  7425  prcunqu  7426  prarloclemlt  7434  genpassl  7465  genpassu  7466  nqprloc  7486  nqpru  7493  appdiv0nq  7505  addcomprg  7519  mulcomprg  7521  distrlem4prl  7525  distrlem4pru  7526  1idprl  7531  1idpru  7532  ltsopr  7537  recexprlemss1l  7576  recexprlemss1u  7577  gt0srpr  7689  mulcomsrg  7698  ltsosr  7705  aptisr  7720  mulextsr1  7722  map2psrprg  7746  axaddcom  7811  axltwlin  7966  axapti  7969  letri3  7979  eqlelt  7985  mul31  8029  cnegexlem3  8075  subval  8090  subcl  8097  pncan2  8105  pncan3  8106  npcan  8107  addsubeq4  8113  npncan3  8136  negsubdi2  8157  muladd  8282  subdi  8283  mulneg2  8294  mulsub  8299  ltleadd  8344  ltsubpos  8352  posdif  8353  addge01  8370  lesub0  8377  reapneg  8495  prodgt02  8748  prodge02  8750  ltdivmul  8771  lerec  8779  lediv2a  8790  le2msq  8796  msq11  8797  lbreu  8840  dfinfre  8851  creur  8854  creui  8855  cju  8856  nnmulcl  8878  nndivtr  8899  avgle1  9097  avgle2  9098  nn0nnaddcl  9145  zletric  9235  zrevaddcl  9241  znnsub  9242  znn0sub  9256  ltsubnn0  9258  zdclt  9268  zextlt  9283  gtndiv  9286  prime  9290  peano5uzti  9299  uztrn2  9483  uztric  9487  uz11  9488  nn0pzuz  9525  indstr  9531  supinfneg  9533  infsupneg  9534  eluzdc  9548  qrevaddcl  9582  difrp  9628  xrltnsym  9729  xrltso  9732  xrlttri3  9733  xrletri3  9740  xleneg  9773  xaddcom  9797  xposdif  9818  ixxssixx  9838  iccid  9861  iooshf  9888  iccsupr  9902  iooneg  9924  iccneg  9925  fztri3or  9974  fzdcel  9975  fzn  9977  fzen  9978  fzass4  9997  fzrev  10019  fznn  10024  elfzp1b  10032  elfzm1b  10033  fz0fzdiffz0  10065  difelfznle  10070  fzon  10101  fzonmapblen  10122  eluzgtdifelfzo  10132  ubmelm1fzo  10161  subfzo0  10177  qletric  10179  ioo0  10195  ico0  10197  ioc0  10198  flqbi  10225  flqbi2  10226  flqzadd  10233  modfzo0difsn  10330  fzfig  10365  expcllem  10466  expap0  10485  mulbinom2  10571  expnbnd  10578  sq11ap  10622  hashfacen  10749  shftlem  10758  shftuz  10759  shftfvalg  10760  ovshftex  10761  shftfval  10763  shftval4  10770  shftval5  10771  2shfti  10773  mulreap  10806  sqrt11ap  10980  abs3dif  11047  abs2difabs  11050  maxabslemval  11150  maxle2  11154  maxclpr  11164  2zsupmax  11167  mingeb  11183  2zinfmin  11184  xrmaxiflemval  11191  xrmax2sup  11195  iooinsup  11218  climshftlemg  11243  fsumcnv  11378  explecnv  11446  geo2lim  11457  prodmodc  11519  fprodcnv  11566  demoivre  11713  demoivreALT  11714  nndivides  11737  0dvds  11751  muldvds1  11756  muldvds2  11757  dvdssubr  11779  dvdsadd2b  11780  odd2np1  11810  mulsucdiv2z  11822  ltoddhalfle  11830  ndvdssub  11867  gcdcom  11906  neggcd  11916  gcdabs2  11923  modgcd  11924  bezoutlemaz  11936  dfgcd2  11947  lcmcom  11996  neglcm  12007  lcmgcdeq  12015  coprmdvds  12024  qredeq  12028  divgcdcoprmex  12034  isprm3  12050  prmind2  12052  dvdsprm  12069  cncongrprm  12089  sqrt2irr  12094  hashgcdeq  12171  modprmn0modprm0  12188  coprimeprodsq  12189  pythagtriplem1  12197  pythagtriplem4  12200  pc2dvds  12261  pc11  12262  pcz  12263  pcprod  12276  prmunb  12292  1arithlem2  12294  1arithlem3  12295  1arith  12297  eltg  12702  eltg2  12703  tgss  12713  tgss2  12729  basgen2  12731  bastop1  12733  opnneiss  12808  cnrest  12885  txss12  12916  hmeofvalg  12953  txswaphmeolem  12970  txswaphmeo  12971  blpnfctr  13089  metequiv  13145  metcnp3  13161  qtopbasss  13171  reopnap  13188  bl2ioo  13192  ioo2bl  13193  ioo2blex  13194  cncfval  13209  divccncfap  13227  addccncf  13236  expcncf  13242  dvexp  13325  dvef  13338  efle  13347  reapef  13349  ptolemy  13395  logleb  13446  lgsprme0  13593  uzdcinzz  13689  exmidsbthrlem  13911  triap  13918