Theorem ancoms 266

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 115	. 2 |- ( ps -> ( ph -> ch ) )
3	2	imp 123	1 |- ( ( ps /\ ph ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  adantl  275  syl2anr  288  anim12ci  337  sylan9bbr  459  anabss4  567  anabsi7  571  anabsi8  572  im2anan9r  589  bi2anan9r  597  syl3anr2  1281  mp3anr1  1324  mp3anr2  1325  mp3anr3  1326  eu5  2061  2exeu  2106  eqeqan12rd  2182  sylan9eqr  2220  r19.29vva  2610  morex  2909  sylan9ssr  3155  riinm  3937  breqan12rd  3998  elnn  4582  soinxp  4673  seinxp  4674  brelrng  4834  dminss  5017  imainss  5018  funsng  5233  funcnvuni  5256  f1co  5404  f1ocnv  5444  fun11iun  5452  funimass4  5536  fndmdifcom  5590  fsn2  5658  fvtp2g  5693  fvtp3g  5694  fvtp2  5696  fvtp3  5697  acexmid  5840  oveqan12rd  5861  cofunex2g  6077  brtposg  6218  tposoprab  6244  smores3  6257  smores2  6258  smoel  6264  tfri3  6331  rdgtfr  6338  rdgruledefgg  6339  omcl  6425  oeicl  6426  nnmsucr  6452  nnmcom  6453  nndir  6454  nnaordi  6472  nnaordr  6474  nnaword  6475  nnmordi  6480  nnaordex  6491  nnm00  6493  ersym  6509  elecg  6535  riinerm  6570  ecopovsym  6593  ecopovsymg  6596  ecovcom  6604  ecovicom  6605  mapvalg  6620  pmvalg  6621  elpmg  6626  elmapssres  6635  pmss12g  6637  ixpconstg  6669  ener  6741  domtr  6747  f1imaeng  6754  fundmen  6768  xpcomco  6788  xpsnen2g  6791  xpdom2  6793  xpdom1g  6795  enen2  6803  domen2  6805  ssfilem  6837  diffitest  6849  fiintim  6890  fundmfibi  6900  cnvti  6980  djuex  7004  nnnninf  7086  ltsopi  7257  pitric  7258  pitri3or  7259  addcompig  7266  mulcompig  7268  ltapig  7275  ltmpig  7276  nnppipi  7280  addcomnqg  7318  addassnqg  7319  distrnqg  7324  recexnq  7327  nqtri3or  7333  ltmnqg  7338  lt2addnq  7341  lt2mulnq  7342  ltbtwnnqq  7352  prarloclemarch2  7356  enq0ref  7370  distrnq0  7396  mulcomnq0  7397  prcdnql  7421  prcunqu  7422  prarloclemlt  7430  genpassl  7461  genpassu  7462  nqprloc  7482  nqpru  7489  appdiv0nq  7501  addcomprg  7515  mulcomprg  7517  distrlem4prl  7521  distrlem4pru  7522  1idprl  7527  1idpru  7528  ltsopr  7533  recexprlemss1l  7572  recexprlemss1u  7573  gt0srpr  7685  mulcomsrg  7694  ltsosr  7701  aptisr  7716  mulextsr1  7718  map2psrprg  7742  axaddcom  7807  axltwlin  7962  axapti  7965  letri3  7975  eqlelt  7981  mul31  8025  cnegexlem3  8071  subval  8086  subcl  8093  pncan2  8101  pncan3  8102  npcan  8103  addsubeq4  8109  npncan3  8132  negsubdi2  8153  muladd  8278  subdi  8279  mulneg2  8290  mulsub  8295  ltleadd  8340  ltsubpos  8348  posdif  8349  addge01  8366  lesub0  8373  reapneg  8491  prodgt02  8744  prodge02  8746  ltdivmul  8767  lerec  8775  lediv2a  8786  le2msq  8792  msq11  8793  lbreu  8836  dfinfre  8847  creur  8850  creui  8851  cju  8852  nnmulcl  8874  nndivtr  8895  avgle1  9093  avgle2  9094  nn0nnaddcl  9141  zletric  9231  zrevaddcl  9237  znnsub  9238  znn0sub  9252  ltsubnn0  9254  zdclt  9264  zextlt  9279  gtndiv  9282  prime  9286  peano5uzti  9295  uztrn2  9479  uztric  9483  uz11  9484  nn0pzuz  9521  indstr  9527  supinfneg  9529  infsupneg  9530  eluzdc  9544  qrevaddcl  9578  difrp  9624  xrltnsym  9725  xrltso  9728  xrlttri3  9729  xrletri3  9736  xleneg  9769  xaddcom  9793  xposdif  9814  ixxssixx  9834  iccid  9857  iooshf  9884  iccsupr  9898  iooneg  9920  iccneg  9921  fztri3or  9970  fzdcel  9971  fzn  9973  fzen  9974  fzass4  9993  fzrev  10015  fznn  10020  elfzp1b  10028  elfzm1b  10029  fz0fzdiffz0  10061  difelfznle  10066  fzon  10097  fzonmapblen  10118  eluzgtdifelfzo  10128  ubmelm1fzo  10157  subfzo0  10173  qletric  10175  ioo0  10191  ico0  10193  ioc0  10194  flqbi  10221  flqbi2  10222  flqzadd  10229  modfzo0difsn  10326  fzfig  10361  expcllem  10462  expap0  10481  mulbinom2  10567  expnbnd  10574  sq11ap  10618  hashfacen  10745  shftlem  10754  shftuz  10755  shftfvalg  10756  ovshftex  10757  shftfval  10759  shftval4  10766  shftval5  10767  2shfti  10769  mulreap  10802  sqrt11ap  10976  abs3dif  11043  abs2difabs  11046  maxabslemval  11146  maxle2  11150  maxclpr  11160  2zsupmax  11163  mingeb  11179  2zinfmin  11180  xrmaxiflemval  11187  xrmax2sup  11191  iooinsup  11214  climshftlemg  11239  fsumcnv  11374  explecnv  11442  geo2lim  11453  prodmodc  11515  fprodcnv  11562  demoivre  11709  demoivreALT  11710  nndivides  11733  0dvds  11747  muldvds1  11752  muldvds2  11753  dvdssubr  11775  dvdsadd2b  11776  odd2np1  11806  mulsucdiv2z  11818  ltoddhalfle  11826  ndvdssub  11863  gcdcom  11902  neggcd  11912  gcdabs2  11919  modgcd  11920  bezoutlemaz  11932  dfgcd2  11943  lcmcom  11992  neglcm  12003  lcmgcdeq  12011  coprmdvds  12020  qredeq  12024  divgcdcoprmex  12030  isprm3  12046  prmind2  12048  dvdsprm  12065  cncongrprm  12085  sqrt2irr  12090  hashgcdeq  12167  modprmn0modprm0  12184  coprimeprodsq  12185  pythagtriplem1  12193  pythagtriplem4  12196  pc2dvds  12257  pc11  12258  pcz  12259  pcprod  12272  prmunb  12288  1arithlem2  12290  1arithlem3  12291  1arith  12293  eltg  12652  eltg2  12653  tgss  12663  tgss2  12679  basgen2  12681  bastop1  12683  opnneiss  12758  cnrest  12835  txss12  12866  hmeofvalg  12903  txswaphmeolem  12920  txswaphmeo  12921  blpnfctr  13039  metequiv  13095  metcnp3  13111  qtopbasss  13121  reopnap  13138  bl2ioo  13142  ioo2bl  13143  ioo2blex  13144  cncfval  13159  divccncfap  13177  addccncf  13186  expcncf  13192  dvexp  13275  dvef  13288  efle  13297  reapef  13299  ptolemy  13345  logleb  13396  lgsprme0  13543  uzdcinzz  13639  exmidsbthrlem  13861  triap  13868