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  3021  sbcrext  3120  sylan9ssr  3287  pssdifcom1  3636  pssdifcom2  3637  riinn0  4041  symdifexg  4104  addcexg  4394  findsd  4411  nnsucelr  4429  nulge  4457  lenltfin  4470  ncfinprop  4475  ncfinlower  4484  tfinltfin  4502  tfinlefin  4503  sfindbl  4531  sfinltfin  4536  sfin111  4537  nulnnn  4557  phi11lem1  4596  breqan12rd  4656  dminss  5042  imainss  5043  dfco2a  5082  funeq  5128  funcnvuni  5162  f1co  5265  fun11iun  5306  fsn2  5435  isotr  5496  oveqan12rd  5543  clos1conn  5880  mapvalg  6010  pmvalg  6011  entr  6039  fndmeng  6047  xpsnen2g  6055  ovmuc  6131  muccom  6135  peano4nc  6151  eqtc  6162  cenc  6182  sbth  6207  dflec2  6211  leltctr  6213  leconnnc  6219  ce2le  6234  nclenn  6250  lemuc1  6254  nnc3n3p2  6280  nchoicelem12  6301  nchoicelem17  6306  fnfrec  6321