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.29_2a  2450  morex  2719  sylan9ssr  2953  sspssn  3042  psssstr  3045  riinm  3719  breqan12rd  3770  elnn  4270  soinxp  4352  seinxp  4353  brelrng  4507  dminss  4680  imainss  4681  funsng  4887  funcnvuni  4909  f1co  5042  f1ocnv  5080  fun11iun  5088  funimass4  5165  fndmdifcom  5214  fsn2  5278  fvtp2g  5311  fvtp3g  5312  fvtp2  5314  fvtp3  5315  acexmid  5451  oveqan12rd  5472  cofunex2g  5678  brtposg  5807  tposoprab  5833  smores3  5846  smores2  5847  smoel  5853  tfri3  5891  rdgtfr  5898  rdgruledefgg  5899  omcl  5973  oeicl  5974  nnmsucr  5999  nnmcom  6000  nndir  6001  nnaordi  6010  nnaordr  6012  nnaword  6013  nnmordi  6018  nnaordex  6029  nnm00  6031  ersym  6047  elecg  6073  riinerm  6108  ecopovsym  6131  ecopovsymg  6134  ecovcom  6142  ecovicom  6143  ener  6188  domtr  6194  f1imaeng  6201  fundmen  6215  xpcomco  6229  xpsnen2g  6232  xpdom2  6234  xpdom1g  6236  enen2  6241  domen2  6243  ssfiexmid  6247  ltsopi  6297  pitric  6298  pitri3or  6299  addcompig  6306  mulcompig  6308  ltapig  6315  ltmpig  6316  nnppipi  6320  addcomnqg  6358  addassnqg  6359  distrnqg  6364  recexnq  6367  nqtri3or  6373  ltmnqg  6378  lt2addnq  6381  ltbtwnnqq  6391  prarloclemarch2  6395  enq0ref  6408  distrnq0  6434  mulcomnq0  6435  prcdnql  6459  prcunqu  6460  prarloclemlt  6468  genpassl  6500  genpassu  6501  nqprloc  6521  appdiv0nq  6535  addcomprg  6544  mulcomprg  6546  distrlem4prl  6550  distrlem4pru  6551  1idprl  6556  1idpru  6557  ltsopr  6560  recexprlemss1l  6597  recexprlemss1u  6598  gt0srpr  6628  mulcomsrg  6637  ltsosr  6644  aptisr  6657  mulextsr1  6659  axaddcom  6706  axltwlin  6836  axapti  6839  letri3  6848  mul31  6893  cnegexlem3  6937  subval  6952  subcl  6959  pncan2  6967  pncan3  6968  npcan  6969  addsubeq4  6975  npncan3  6997  negsubdi2  7018  muladd  7129  subdi  7130  mulneg2  7141  mulsub  7146  ltleadd  7188  ltsubpos  7196  posdif  7197  addge01  7214  lesub0  7221  reapneg  7333  prodgt02  7551  prodge02  7553  ltdivmul  7574  lerec  7582  lediv2a  7593  le2msq  7599  msq11  7600  creur  7643  creui  7644  cju  7645  nnmulcl  7667  nndivtr  7687  avgle1  7892  avgle2  7893  nn0nnaddcl  7939  zletric  8015  zrevaddcl  8021  znnsub  8022  znn0sub  8035  zextlt  8057  gtndiv  8060  prime  8062  peano5uzti  8071  uztrn2  8215  uztric  8219  uz11  8220  nn0pzuz  8255  indstr  8261  eluzdc  8272  qrevaddcl  8302  difrp  8342  xrltnsym  8432  xrltso  8435  xrlttri3  8436  xrletri3  8439  xleneg  8468  ixxssixx  8489  iccid  8512  iooshf  8539  iccsupr  8553  iooneg  8574  iccneg  8575  fzn  8622  fzen  8623  fzass4  8641  fzrev  8662  fznn  8667  elfzp1b  8675  elfzm1b  8676  fz0fzdiffz0  8703  difelfznle  8709  fzon  8738  fzonmapblen  8759  eluzgtdifelfzo  8769  ubmelm1fzo  8798  fzfig  8825