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  1280  mp3anr1  1323  mp3anr2  1324  mp3anr3  1325  eu5  2060  2exeu  2105  eqeqan12rd  2181  sylan9eqr  2219  r19.29vva  2609  morex  2905  sylan9ssr  3151  riinm  3932  breqan12rd  3993  elnn  4577  soinxp  4668  seinxp  4669  brelrng  4829  dminss  5012  imainss  5013  funsng  5228  funcnvuni  5251  f1co  5399  f1ocnv  5439  fun11iun  5447  funimass4  5531  fndmdifcom  5585  fsn2  5653  fvtp2g  5688  fvtp3g  5689  fvtp2  5691  fvtp3  5692  acexmid  5835  oveqan12rd  5856  cofunex2g  6072  brtposg  6213  tposoprab  6239  smores3  6252  smores2  6253  smoel  6259  tfri3  6326  rdgtfr  6333  rdgruledefgg  6334  omcl  6420  oeicl  6421  nnmsucr  6447  nnmcom  6448  nndir  6449  nnaordi  6467  nnaordr  6469  nnaword  6470  nnmordi  6475  nnaordex  6486  nnm00  6488  ersym  6504  elecg  6530  riinerm  6565  ecopovsym  6588  ecopovsymg  6591  ecovcom  6599  ecovicom  6600  mapvalg  6615  pmvalg  6616  elpmg  6621  elmapssres  6630  pmss12g  6632  ixpconstg  6664  ener  6736  domtr  6742  f1imaeng  6749  fundmen  6763  xpcomco  6783  xpsnen2g  6786  xpdom2  6788  xpdom1g  6790  enen2  6798  domen2  6800  ssfilem  6832  diffitest  6844  fiintim  6885  fundmfibi  6895  cnvti  6975  djuex  6999  nnnninf  7081  ltsopi  7252  pitric  7253  pitri3or  7254  addcompig  7261  mulcompig  7263  ltapig  7270  ltmpig  7271  nnppipi  7275  addcomnqg  7313  addassnqg  7314  distrnqg  7319  recexnq  7322  nqtri3or  7328  ltmnqg  7333  lt2addnq  7336  lt2mulnq  7337  ltbtwnnqq  7347  prarloclemarch2  7351  enq0ref  7365  distrnq0  7391  mulcomnq0  7392  prcdnql  7416  prcunqu  7417  prarloclemlt  7425  genpassl  7456  genpassu  7457  nqprloc  7477  nqpru  7484  appdiv0nq  7496  addcomprg  7510  mulcomprg  7512  distrlem4prl  7516  distrlem4pru  7517  1idprl  7522  1idpru  7523  ltsopr  7528  recexprlemss1l  7567  recexprlemss1u  7568  gt0srpr  7680  mulcomsrg  7689  ltsosr  7696  aptisr  7711  mulextsr1  7713  map2psrprg  7737  axaddcom  7802  axltwlin  7957  axapti  7960  letri3  7970  eqlelt  7976  mul31  8020  cnegexlem3  8066  subval  8081  subcl  8088  pncan2  8096  pncan3  8097  npcan  8098  addsubeq4  8104  npncan3  8127  negsubdi2  8148  muladd  8273  subdi  8274  mulneg2  8285  mulsub  8290  ltleadd  8335  ltsubpos  8343  posdif  8344  addge01  8361  lesub0  8368  reapneg  8486  prodgt02  8739  prodge02  8741  ltdivmul  8762  lerec  8770  lediv2a  8781  le2msq  8787  msq11  8788  lbreu  8831  dfinfre  8842  creur  8845  creui  8846  cju  8847  nnmulcl  8869  nndivtr  8890  avgle1  9088  avgle2  9089  nn0nnaddcl  9136  zletric  9226  zrevaddcl  9232  znnsub  9233  znn0sub  9247  ltsubnn0  9249  zdclt  9259  zextlt  9274  gtndiv  9277  prime  9281  peano5uzti  9290  uztrn2  9474  uztric  9478  uz11  9479  nn0pzuz  9516  indstr  9522  supinfneg  9524  infsupneg  9525  eluzdc  9539  qrevaddcl  9573  difrp  9619  xrltnsym  9720  xrltso  9723  xrlttri3  9724  xrletri3  9731  xleneg  9764  xaddcom  9788  xposdif  9809  ixxssixx  9829  iccid  9852  iooshf  9879  iccsupr  9893  iooneg  9915  iccneg  9916  fztri3or  9964  fzdcel  9965  fzn  9967  fzen  9968  fzass4  9987  fzrev  10009  fznn  10014  elfzp1b  10022  elfzm1b  10023  fz0fzdiffz0  10055  difelfznle  10060  fzon  10091  fzonmapblen  10112  eluzgtdifelfzo  10122  ubmelm1fzo  10151  subfzo0  10167  qletric  10169  ioo0  10185  ico0  10187  ioc0  10188  flqbi  10215  flqbi2  10216  flqzadd  10223  modfzo0difsn  10320  fzfig  10355  expcllem  10456  expap0  10475  mulbinom2  10560  expnbnd  10567  sq11ap  10611  hashfacen  10735  shftlem  10744  shftuz  10745  shftfvalg  10746  ovshftex  10747  shftfval  10749  shftval4  10756  shftval5  10757  2shfti  10759  mulreap  10792  sqrt11ap  10966  abs3dif  11033  abs2difabs  11036  maxabslemval  11136  maxle2  11140  maxclpr  11150  2zsupmax  11153  mingeb  11169  2zinfmin  11170  xrmaxiflemval  11177  xrmax2sup  11181  iooinsup  11204  climshftlemg  11229  fsumcnv  11364  explecnv  11432  geo2lim  11443  prodmodc  11505  fprodcnv  11552  demoivre  11699  demoivreALT  11700  nndivides  11723  0dvds  11737  muldvds1  11742  muldvds2  11743  dvdssubr  11764  dvdsadd2b  11765  odd2np1  11795  mulsucdiv2z  11807  ltoddhalfle  11815  ndvdssub  11852  gcdcom  11891  neggcd  11901  gcdabs2  11908  modgcd  11909  bezoutlemaz  11921  dfgcd2  11932  lcmcom  11975  neglcm  11986  lcmgcdeq  11994  coprmdvds  12003  qredeq  12007  divgcdcoprmex  12013  isprm3  12029  prmind2  12031  dvdsprm  12048  cncongrprm  12066  sqrt2irr  12071  hashgcdeq  12148  modprmn0modprm0  12165  coprimeprodsq  12166  pythagtriplem1  12174  pythagtriplem4  12177  pc2dvds  12238  pc11  12239  pcz  12240  pcprod  12253  eltg  12593  eltg2  12594  tgss  12604  tgss2  12620  basgen2  12622  bastop1  12624  opnneiss  12699  cnrest  12776  txss12  12807  hmeofvalg  12844  txswaphmeolem  12861  txswaphmeo  12862  blpnfctr  12980  metequiv  13036  metcnp3  13052  qtopbasss  13062  reopnap  13079  bl2ioo  13083  ioo2bl  13084  ioo2blex  13085  cncfval  13100  divccncfap  13118  addccncf  13127  expcncf  13133  dvexp  13216  dvef  13229  efle  13238  reapef  13240  ptolemy  13286  logleb  13337  uzdcinzz  13514  exmidsbthrlem  13735  triap  13742