Theorem ancoms 255

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 109	. 2 ⊢ (ψ → (φ → χ))
3	2	imp 115	1 ⊢ ((ψ ∧ φ) → χ)

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  adantl  262  syl2anr  274  anim12ci  322  sylan9bbr  436  anabss4  511  anabsi7  515  anabsi8  516  im2anan9r  531  bi2anan9r  539  syl3anr2  1187  mp3anr1  1228  mp3anr2  1229  mp3anr3  1230  eu5  1944  2exeu  1989  eqeqan12rd  2053  sylan9eqr  2091  r19.29vva  2450  morex  2719  sylan9ssr  2953  sspssn  3042  psssstr  3045  riinm  3720  breqan12rd  3771  elnn  4271  soinxp  4353  seinxp  4354  brelrng  4508  dminss  4681  imainss  4682  funsng  4889  funcnvuni  4911  f1co  5044  f1ocnv  5082  fun11iun  5090  funimass4  5167  fndmdifcom  5216  fsn2  5280  fvtp2g  5313  fvtp3g  5314  fvtp2  5316  fvtp3  5317  acexmid  5454  oveqan12rd  5475  cofunex2g  5681  brtposg  5810  tposoprab  5836  smores3  5849  smores2  5850  smoel  5856  tfri3  5894  rdgtfr  5901  rdgruledefgg  5902  omcl  5980  oeicl  5981  nnmsucr  6006  nnmcom  6007  nndir  6008  nnaordi  6017  nnaordr  6019  nnaword  6020  nnmordi  6025  nnaordex  6036  nnm00  6038  ersym  6054  elecg  6080  riinerm  6115  ecopovsym  6138  ecopovsymg  6141  ecovcom  6149  ecovicom  6150  ener  6195  domtr  6201  f1imaeng  6208  fundmen  6222  xpcomco  6236  xpsnen2g  6239  xpdom2  6241  xpdom1g  6243  enen2  6248  domen2  6250  ssfiexmid  6254  ltsopi  6304  pitric  6305  pitri3or  6306  addcompig  6313  mulcompig  6315  ltapig  6322  ltmpig  6323  nnppipi  6327  addcomnqg  6365  addassnqg  6366  distrnqg  6371  recexnq  6374  nqtri3or  6380  ltmnqg  6385  lt2addnq  6388  ltbtwnnqq  6398  prarloclemarch2  6402  enq0ref  6416  distrnq0  6442  mulcomnq0  6443  prcdnql  6467  prcunqu  6468  prarloclemlt  6476  genpassl  6507  genpassu  6508  nqprloc  6528  appdiv0nq  6545  addcomprg  6554  mulcomprg  6556  distrlem4prl  6560  distrlem4pru  6561  1idprl  6566  1idpru  6567  ltsopr  6570  recexprlemss1l  6607  recexprlemss1u  6608  gt0srpr  6676  mulcomsrg  6685  ltsosr  6692  aptisr  6705  mulextsr1  6707  axaddcom  6754  axltwlin  6884  axapti  6887  letri3  6896  mul31  6941  cnegexlem3  6985  subval  7000  subcl  7007  pncan2  7015  pncan3  7016  npcan  7017  addsubeq4  7023  npncan3  7045  negsubdi2  7066  muladd  7177  subdi  7178  mulneg2  7189  mulsub  7194  ltleadd  7236  ltsubpos  7244  posdif  7245  addge01  7262  lesub0  7269  reapneg  7381  prodgt02  7600  prodge02  7602  ltdivmul  7623  lerec  7631  lediv2a  7642  le2msq  7648  msq11  7649  creur  7692  creui  7693  cju  7694  nnmulcl  7716  nndivtr  7736  avgle1  7942  avgle2  7943  nn0nnaddcl  7989  zletric  8065  zrevaddcl  8071  znnsub  8072  znn0sub  8085  zdclt  8094  zextlt  8108  gtndiv  8111  prime  8113  peano5uzti  8122  uztrn2  8266  uztric  8270  uz11  8271  nn0pzuz  8306  indstr  8312  eluzdc  8323  qrevaddcl  8353  difrp  8394  xrltnsym  8484  xrltso  8487  xrlttri3  8488  xrletri3  8491  xleneg  8520  ixxssixx  8541  iccid  8564  iooshf  8591  iccsupr  8605  iooneg  8626  iccneg  8627  fztri3or  8673  fzdcel  8674  fzn  8676  fzen  8677  fzass4  8695  fzrev  8716  fznn  8721  elfzp1b  8729  elfzm1b  8730  fz0fzdiffz0  8757  difelfznle  8763  fzon  8792  fzonmapblen  8813  eluzgtdifelfzo  8823  ubmelm1fzo  8852  fzfig  8887  expcllem  8920  expap0  8939  expnbnd  9025  mulreap  9092