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  458  anabss4  566  anabsi7  570  anabsi8  571  im2anan9r  588  bi2anan9r  596  syl3anr2  1269  mp3anr1  1312  mp3anr2  1313  mp3anr3  1314  eu5  2046  2exeu  2091  eqeqan12rd  2156  sylan9eqr  2194  r19.29vva  2577  morex  2868  sylan9ssr  3111  riinm  3885  breqan12rd  3946  elnn  4519  soinxp  4609  seinxp  4610  brelrng  4770  dminss  4953  imainss  4954  funsng  5169  funcnvuni  5192  f1co  5340  f1ocnv  5380  fun11iun  5388  funimass4  5472  fndmdifcom  5526  fsn2  5594  fvtp2g  5629  fvtp3g  5630  fvtp2  5632  fvtp3  5633  acexmid  5773  oveqan12rd  5794  cofunex2g  6010  brtposg  6151  tposoprab  6177  smores3  6190  smores2  6191  smoel  6197  tfri3  6264  rdgtfr  6271  rdgruledefgg  6272  omcl  6357  oeicl  6358  nnmsucr  6384  nnmcom  6385  nndir  6386  nnaordi  6404  nnaordr  6406  nnaword  6407  nnmordi  6412  nnaordex  6423  nnm00  6425  ersym  6441  elecg  6467  riinerm  6502  ecopovsym  6525  ecopovsymg  6528  ecovcom  6536  ecovicom  6537  mapvalg  6552  pmvalg  6553  elpmg  6558  elmapssres  6567  pmss12g  6569  ixpconstg  6601  ener  6673  domtr  6679  f1imaeng  6686  fundmen  6700  xpcomco  6720  xpsnen2g  6723  xpdom2  6725  xpdom1g  6727  enen2  6735  domen2  6737  ssfilem  6769  diffitest  6781  fiintim  6817  fundmfibi  6827  cnvti  6906  djuex  6928  nnnninf  7023  ltsopi  7128  pitric  7129  pitri3or  7130  addcompig  7137  mulcompig  7139  ltapig  7146  ltmpig  7147  nnppipi  7151  addcomnqg  7189  addassnqg  7190  distrnqg  7195  recexnq  7198  nqtri3or  7204  ltmnqg  7209  lt2addnq  7212  lt2mulnq  7213  ltbtwnnqq  7223  prarloclemarch2  7227  enq0ref  7241  distrnq0  7267  mulcomnq0  7268  prcdnql  7292  prcunqu  7293  prarloclemlt  7301  genpassl  7332  genpassu  7333  nqprloc  7353  nqpru  7360  appdiv0nq  7372  addcomprg  7386  mulcomprg  7388  distrlem4prl  7392  distrlem4pru  7393  1idprl  7398  1idpru  7399  ltsopr  7404  recexprlemss1l  7443  recexprlemss1u  7444  gt0srpr  7556  mulcomsrg  7565  ltsosr  7572  aptisr  7587  mulextsr1  7589  map2psrprg  7613  axaddcom  7678  axltwlin  7832  axapti  7835  letri3  7845  mul31  7893  cnegexlem3  7939  subval  7954  subcl  7961  pncan2  7969  pncan3  7970  npcan  7971  addsubeq4  7977  npncan3  8000  negsubdi2  8021  muladd  8146  subdi  8147  mulneg2  8158  mulsub  8163  ltleadd  8208  ltsubpos  8216  posdif  8217  addge01  8234  lesub0  8241  reapneg  8359  prodgt02  8611  prodge02  8613  ltdivmul  8634  lerec  8642  lediv2a  8653  le2msq  8659  msq11  8660  lbreu  8703  dfinfre  8714  creur  8717  creui  8718  cju  8719  nnmulcl  8741  nndivtr  8762  avgle1  8960  avgle2  8961  nn0nnaddcl  9008  zletric  9098  zrevaddcl  9104  znnsub  9105  znn0sub  9119  zdclt  9128  zextlt  9143  gtndiv  9146  prime  9150  peano5uzti  9159  uztrn2  9343  uztric  9347  uz11  9348  nn0pzuz  9382  indstr  9388  supinfneg  9390  infsupneg  9391  eluzdc  9404  qrevaddcl  9436  difrp  9480  xrltnsym  9579  xrltso  9582  xrlttri3  9583  xrletri3  9588  xleneg  9620  xaddcom  9644  xposdif  9665  ixxssixx  9685  iccid  9708  iooshf  9735  iccsupr  9749  iooneg  9771  iccneg  9772  fztri3or  9819  fzdcel  9820  fzn  9822  fzen  9823  fzass4  9842  fzrev  9864  fznn  9869  elfzp1b  9877  elfzm1b  9878  fz0fzdiffz0  9907  difelfznle  9912  fzon  9943  fzonmapblen  9964  eluzgtdifelfzo  9974  ubmelm1fzo  10003  subfzo0  10019  qletric  10021  ioo0  10037  ico0  10039  ioc0  10040  flqbi  10063  flqbi2  10064  flqzadd  10071  modfzo0difsn  10168  fzfig  10203  expcllem  10304  expap0  10323  mulbinom2  10408  expnbnd  10415  sq11ap  10458  hashfacen  10579  shftlem  10588  shftuz  10589  shftfvalg  10590  ovshftex  10591  shftfval  10593  shftval4  10600  shftval5  10601  2shfti  10603  mulreap  10636  sqrt11ap  10810  abs3dif  10877  abs2difabs  10880  maxabslemval  10980  maxle2  10984  maxclpr  10994  2zsupmax  10997  xrmaxiflemval  11019  xrmax2sup  11023  iooinsup  11046  climshftlemg  11071  fsumcnv  11206  explecnv  11274  geo2lim  11285  prodmodc  11347  efler  11405  demoivre  11479  demoivreALT  11480  nndivides  11500  0dvds  11513  muldvds1  11518  muldvds2  11519  dvdssubr  11539  dvdsadd2b  11540  odd2np1  11570  mulsucdiv2z  11582  ltoddhalfle  11590  ndvdssub  11627  gcdcom  11662  neggcd  11671  gcdabs2  11678  modgcd  11679  bezoutlemaz  11691  dfgcd2  11702  lcmcom  11745  neglcm  11756  lcmgcdeq  11764  coprmdvds  11773  qredeq  11777  divgcdcoprmex  11783  isprm3  11799  prmind2  11801  dvdsprm  11817  cncongrprm  11835  sqrt2irr  11840  hashgcdeq  11904  eltg  12221  eltg2  12222  tgss  12232  tgss2  12248  basgen2  12250  bastop1  12252  opnneiss  12327  cnrest  12404  txss12  12435  hmeofvalg  12472  txswaphmeolem  12489  txswaphmeo  12490  blpnfctr  12608  metequiv  12664  metcnp3  12680  qtopbasss  12690  reopnap  12707  bl2ioo  12711  ioo2bl  12712  ioo2blex  12713  cncfval  12728  divccncfap  12746  addccncf  12755  expcncf  12761  dvexp  12844  dvef  12856  ptolemy  12905  uzdcinzz  13005  exmidsbthrlem  13217  triap  13224