Theorem ancoms 264

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  adantl  271  syl2anr  284  anim12ci  332  sylan9bbr  451  anabss4  542  anabsi7  546  anabsi8  547  im2anan9r  564  bi2anan9r  572  syl3anr2  1225  mp3anr1  1268  mp3anr2  1269  mp3anr3  1270  eu5  1992  2exeu  2037  eqeqan12rd  2101  sylan9eqr  2139  r19.29vva  2509  morex  2790  sylan9ssr  3028  riinm  3787  breqan12rd  3838  elnn  4395  soinxp  4478  seinxp  4479  brelrng  4636  dminss  4814  imainss  4815  funsng  5027  funcnvuni  5050  f1co  5193  f1ocnv  5231  fun11iun  5239  funimass4  5320  fndmdifcom  5370  fsn2  5436  fvtp2g  5469  fvtp3g  5470  fvtp2  5472  fvtp3  5473  acexmid  5614  oveqan12rd  5635  cofunex2g  5842  brtposg  5975  tposoprab  6001  smores3  6014  smores2  6015  smoel  6021  tfri3  6088  rdgtfr  6095  rdgruledefgg  6096  omcl  6178  oeicl  6179  nnmsucr  6205  nnmcom  6206  nndir  6207  nnaordi  6221  nnaordr  6223  nnaword  6224  nnmordi  6229  nnaordex  6240  nnm00  6242  ersym  6258  elecg  6284  riinerm  6319  ecopovsym  6342  ecopovsymg  6345  ecovcom  6353  ecovicom  6354  mapvalg  6369  pmvalg  6370  elpmg  6375  elmapssres  6384  pmss12g  6386  ener  6450  domtr  6456  f1imaeng  6463  fundmen  6477  xpcomco  6496  xpsnen2g  6499  xpdom2  6501  xpdom1g  6503  enen2  6511  domen2  6513  ssfilem  6545  diffitest  6557  fundmfibi  6601  cnvti  6661  djuex  6683  nnnninf  6753  ltsopi  6826  pitric  6827  pitri3or  6828  addcompig  6835  mulcompig  6837  ltapig  6844  ltmpig  6845  nnppipi  6849  addcomnqg  6887  addassnqg  6888  distrnqg  6893  recexnq  6896  nqtri3or  6902  ltmnqg  6907  lt2addnq  6910  lt2mulnq  6911  ltbtwnnqq  6921  prarloclemarch2  6925  enq0ref  6939  distrnq0  6965  mulcomnq0  6966  prcdnql  6990  prcunqu  6991  prarloclemlt  6999  genpassl  7030  genpassu  7031  nqprloc  7051  nqpru  7058  appdiv0nq  7070  addcomprg  7084  mulcomprg  7086  distrlem4prl  7090  distrlem4pru  7091  1idprl  7096  1idpru  7097  ltsopr  7102  recexprlemss1l  7141  recexprlemss1u  7142  gt0srpr  7241  mulcomsrg  7250  ltsosr  7257  aptisr  7271  mulextsr1  7273  axaddcom  7352  axltwlin  7501  axapti  7504  letri3  7513  mul31  7560  cnegexlem3  7606  subval  7621  subcl  7628  pncan2  7636  pncan3  7637  npcan  7638  addsubeq4  7644  npncan3  7667  negsubdi2  7688  muladd  7809  subdi  7810  mulneg2  7821  mulsub  7826  ltleadd  7871  ltsubpos  7879  posdif  7880  addge01  7897  lesub0  7904  reapneg  8018  prodgt02  8252  prodge02  8254  ltdivmul  8275  lerec  8283  lediv2a  8294  le2msq  8300  msq11  8301  lbreu  8344  dfinfre  8355  creur  8357  creui  8358  cju  8359  nnmulcl  8381  nndivtr  8401  avgle1  8592  avgle2  8593  nn0nnaddcl  8640  zletric  8730  zrevaddcl  8736  znnsub  8737  znn0sub  8751  zdclt  8760  zextlt  8774  gtndiv  8777  prime  8781  peano5uzti  8790  uztrn2  8971  uztric  8975  uz11  8976  nn0pzuz  9010  indstr  9016  supinfneg  9018  infsupneg  9019  eluzdc  9032  qrevaddcl  9064  difrp  9105  xrltnsym  9198  xrltso  9201  xrlttri3  9202  xrletri3  9205  xleneg  9234  ixxssixx  9255  iccid  9278  iooshf  9305  iccsupr  9319  iooneg  9340  iccneg  9341  fztri3or  9388  fzdcel  9389  fzn  9391  fzen  9392  fzass4  9410  fzrev  9431  fznn  9436  elfzp1b  9444  elfzm1b  9445  fz0fzdiffz0  9472  difelfznle  9477  fzon  9508  fzonmapblen  9529  eluzgtdifelfzo  9539  ubmelm1fzo  9568  subfzo0  9584  qletric  9586  ioo0  9602  ico0  9604  ioc0  9605  flqbi  9628  flqbi2  9629  flqzadd  9636  modfzo0difsn  9733  fzfig  9768  expcllem  9868  expap0  9887  mulbinom2  9970  expnbnd  9977  sq11ap  10020  hashfacen  10141  shftlem  10150  shftuz  10151  shftfvalg  10152  ovshftex  10153  shftfval  10155  shftval4  10162  shftval5  10163  2shfti  10165  mulreap  10197  sqrt11ap  10370  abs3dif  10437  abs2difabs  10440  maxabslemval  10540  maxle2  10544  maxclpr  10554  climshftlemg  10588  nndivides  10709  0dvds  10722  muldvds1  10727  muldvds2  10728  dvdssubr  10748  dvdsadd2b  10749  odd2np1  10779  mulsucdiv2z  10791  ltoddhalfle  10799  ndvdssub  10836  gcdcom  10871  neggcd  10880  gcdabs2  10887  modgcd  10888  bezoutlemaz  10898  dfgcd2  10909  lcmcom  10952  neglcm  10963  lcmgcdeq  10971  coprmdvds  10980  qredeq  10984  divgcdcoprmex  10990  isprm3  11006  prmind2  11008  dvdsprm  11024  cncongrprm  11042  sqrt2irr  11047  hashgcdeq  11110  uzdcinzz  11167  exmidsbthrlem  11381