Theorem ancoms 255

Description: Inference commuting conjunction in antecedent. (Contributed by NM, 21-Apr-1994.)

Hypothesis

Ref	Expression
ancoms.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
ancoms	|- ( ( ps /\ ph ) -> ch )

Proof of Theorem ancoms

Step	Hyp	Ref	Expression
1		ancoms.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	expcom 109	. 2 |- ( ps -> ( ph -> ch ) )
3	2	imp 115	1 |- ( ( ps /\ ph ) -> ch )

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  1188  mp3anr1  1229  mp3anr2  1230  mp3anr3  1231  eu5  1947  2exeu  1992  eqeqan12rd  2056  sylan9eqr  2094  r19.29vva  2456  morex  2725  sylan9ssr  2959  sspssn  3048  psssstr  3051  riinm  3729  breqan12rd  3780  elnn  4328  soinxp  4410  seinxp  4411  brelrng  4565  dminss  4738  imainss  4739  funsng  4946  funcnvuni  4968  f1co  5101  f1ocnv  5139  fun11iun  5147  funimass4  5224  fndmdifcom  5273  fsn2  5337  fvtp2g  5370  fvtp3g  5371  fvtp2  5373  fvtp3  5374  acexmid  5511  oveqan12rd  5532  cofunex2g  5739  brtposg  5869  tposoprab  5895  smores3  5908  smores2  5909  smoel  5915  tfri3  5953  rdgtfr  5961  rdgruledefgg  5962  omcl  6041  oeicl  6042  nnmsucr  6067  nnmcom  6068  nndir  6069  nnaordi  6081  nnaordr  6083  nnaword  6084  nnmordi  6089  nnaordex  6100  nnm00  6102  ersym  6118  elecg  6144  riinerm  6179  ecopovsym  6202  ecopovsymg  6205  ecovcom  6213  ecovicom  6214  ener  6259  domtr  6265  f1imaeng  6272  fundmen  6286  xpcomco  6300  xpsnen2g  6303  xpdom2  6305  xpdom1g  6307  enen2  6312  domen2  6314  ssfiexmid  6336  diffitest  6344  ltsopi  6418  pitric  6419  pitri3or  6420  addcompig  6427  mulcompig  6429  ltapig  6436  ltmpig  6437  nnppipi  6441  addcomnqg  6479  addassnqg  6480  distrnqg  6485  recexnq  6488  nqtri3or  6494  ltmnqg  6499  lt2addnq  6502  lt2mulnq  6503  ltbtwnnqq  6513  prarloclemarch2  6517  enq0ref  6531  distrnq0  6557  mulcomnq0  6558  prcdnql  6582  prcunqu  6583  prarloclemlt  6591  genpassl  6622  genpassu  6623  nqprloc  6643  nqpru  6650  appdiv0nq  6662  addcomprg  6676  mulcomprg  6678  distrlem4prl  6682  distrlem4pru  6683  1idprl  6688  1idpru  6689  ltsopr  6694  recexprlemss1l  6733  recexprlemss1u  6734  gt0srpr  6833  mulcomsrg  6842  ltsosr  6849  aptisr  6863  mulextsr1  6865  axaddcom  6944  axltwlin  7087  axapti  7090  letri3  7099  mul31  7144  cnegexlem3  7188  subval  7203  subcl  7210  pncan2  7218  pncan3  7219  npcan  7220  addsubeq4  7226  npncan3  7249  negsubdi2  7270  muladd  7381  subdi  7382  mulneg2  7393  mulsub  7398  ltleadd  7441  ltsubpos  7449  posdif  7450  addge01  7467  lesub0  7474  reapneg  7588  prodgt02  7819  prodge02  7821  ltdivmul  7842  lerec  7850  lediv2a  7861  le2msq  7867  msq11  7868  creur  7911  creui  7912  cju  7913  nnmulcl  7935  nndivtr  7955  avgle1  8165  avgle2  8166  nn0nnaddcl  8213  zletric  8289  zrevaddcl  8295  znnsub  8296  znn0sub  8309  zdclt  8318  zextlt  8332  gtndiv  8335  prime  8337  peano5uzti  8346  uztrn2  8490  uztric  8494  uz11  8495  nn0pzuz  8530  indstr  8536  eluzdc  8547  qrevaddcl  8578  difrp  8619  xrltnsym  8714  xrltso  8717  xrlttri3  8718  xrletri3  8721  xleneg  8750  ixxssixx  8771  iccid  8794  iooshf  8821  iccsupr  8835  iooneg  8856  iccneg  8857  fztri3or  8903  fzdcel  8904  fzn  8906  fzen  8907  fzass4  8925  fzrev  8946  fznn  8951  elfzp1b  8959  elfzm1b  8960  fz0fzdiffz0  8987  difelfznle  8993  fzon  9022  fzonmapblen  9043  eluzgtdifelfzo  9053  ubmelm1fzo  9082  subfzo0  9097  qletric  9099  flqbi  9132  flqbi2  9133  flqzadd  9140  fzfig  9206  expcllem  9266  expap0  9285  expnbnd  9372  sq11ap  9414  shftlem  9417  shftuz  9418  shftfvalg  9419  ovshftex  9420  shftfval  9422  shftval4  9429  shftval5  9430  2shfti  9432  mulreap  9464  sqrt11ap  9636  abs3dif  9701  abs2difabs  9704  climshftlemg  9823  sqrt2irr  9878