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  439  anabss4  498  anabsi7  502  anabsi8  503  im2anan9r  518  bi2anan9r  527  syl3anr2  1174  mp3anr1  1214  mp3anr2  1215  mp3anr3  1216  eu5  1929  2exeu  1974  eqeqan12rd  2038  sylan9eqr  2076  r19.29_2a  2434  morex  2702  sylan9ssr  2936  sspssn  3025  psssstr  3028  riinm  3703  breqan12rd  3754  elnn  4255  soinxp  4337  seinxp  4338  brelrng  4492  dminss  4665  imainss  4666  funsng  4872  funcnvuni  4894  f1co  5026  f1ocnv  5064  fun11iun  5072  funimass4  5149  fndmdifcom  5198  fsn2  5262  fvtp2g  5295  fvtp3g  5296  fvtp2  5298  fvtp3  5299  acexmid  5435  oveqan12rd  5456  cofunex2g  5662  brtposg  5791  tposoprab  5817  smores3  5830  smores2  5831  smoel  5837  tfri3  5875  rdgruledefgg  5882  omcl  5956  oeicl  5957  nnmsucr  5982  nnmcom  5983  nndir  5984  nnaordi  5992  nnaordr  5994  nnaword  5995  nnmordi  6000  nnaordex  6011  nnm00  6013  ersym  6029  elecg  6055  riinerm  6090  ecopovsym  6113  ecopovsymg  6116  ecovcom  6124  ecovicom  6125  ltsopi  6180  pitric  6181  pitri3or  6182  addcompig  6189  mulcompig  6191  ltapig  6198  ltmpig  6199  nnppipi  6202  addcomnqg  6240  addassnqg  6241  distrnqg  6246  recex  6249  nqtri3or  6255  ltmnqg  6260  lt2addnq  6263  ltbtwnnqq  6272  prarloclemarch2  6276  enq0ref  6288  distrnq0  6314  mulcomnq0  6315  prcdnql  6338  prcunqu  6339  prarloclemlt  6347  genpassl  6379  genpassu  6380  nqprloc  6400  appdiv0nq  6408  addcomprg  6417  mulcomprg  6419  distrlem4prl  6423  distrlem4pru  6424  1idprl  6429  1idpru  6430  ltsopr  6433  recexprlemss1l  6469  recexprlemss1u  6470  gt0srpr  6495  mulcomsrg  6504  ltsosr  6511  axaddcom  6564  axltwlin  6688  mul31  6731  cnegexlem3  6775  subval  6790  subcl  6797  pncan2  6805  pncan3  6806  npcan  6807  addsubeq4  6813  npncan3  6835  negsubdi2  6856  muladd  6967  subdi  6968  mulneg2  6979  mulsub  6984