Theorem ancoms 439

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

Syntax hints:   → wi 4   ∧ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  adantl  452  syl2anr  464  anim12ci  550  sylan9bbr  681  anabss4  788  anabsi7  792  anabsi8  793  im2anan9r  809  bi2anan9r  844  syl3anr2  1235  mp3anr1  1274  mp3anr2  1275  mp3anr3  1276  19.29r  1597  nfeud2  2216  2eu1  2284  2eu3  2286  eqeqan12rd  2369  sylan9eqr  2407  morex  3020  sbcrext  3119  sylan9ssr  3286  pssdifcom1  3635  pssdifcom2  3636  riinn0  4040  symdifexg  4103  addcexg  4393  findsd  4410  nnsucelr  4428  nulge  4456  lenltfin  4469  ncfinprop  4474  ncfinlower  4483  tfinltfin  4501  tfinlefin  4502  sfindbl  4530  sfinltfin  4535  sfin111  4536  nulnnn  4556  phi11lem1  4595  breqan12rd  4655  dminss  5041  imainss  5042  dfco2a  5081  funeq  5127  funcnvuni  5161  f1co  5264  fun11iun  5305  fsn2  5434  isotr  5495  oveqan12rd  5542  clos1conn  5879  mapvalg  6009  pmvalg  6010  entr  6038  fndmeng  6046  xpsnen2g  6054  ovmuc  6130  muccom  6134  peano4nc  6150  eqtc  6161  cenc  6181  sbth  6206  dflec2  6210  leltctr  6212  leconnnc  6218  ce2le  6233  nclenn  6249  lemuc1  6253  nnc3n3p2  6279  nchoicelem12  6300  nchoicelem17  6305  fnfrec  6320