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  1273  mp3anr1  1316  mp3anr2  1317  mp3anr3  1318  eu5  2053  2exeu  2098  eqeqan12rd  2174  sylan9eqr  2212  r19.29vva  2602  morex  2896  sylan9ssr  3142  riinm  3923  breqan12rd  3984  elnn  4568  soinxp  4659  seinxp  4660  brelrng  4820  dminss  5003  imainss  5004  funsng  5219  funcnvuni  5242  f1co  5390  f1ocnv  5430  fun11iun  5438  funimass4  5522  fndmdifcom  5576  fsn2  5644  fvtp2g  5679  fvtp3g  5680  fvtp2  5682  fvtp3  5683  acexmid  5826  oveqan12rd  5847  cofunex2g  6063  brtposg  6204  tposoprab  6230  smores3  6243  smores2  6244  smoel  6250  tfri3  6317  rdgtfr  6324  rdgruledefgg  6325  omcl  6411  oeicl  6412  nnmsucr  6438  nnmcom  6439  nndir  6440  nnaordi  6458  nnaordr  6460  nnaword  6461  nnmordi  6466  nnaordex  6477  nnm00  6479  ersym  6495  elecg  6521  riinerm  6556  ecopovsym  6579  ecopovsymg  6582  ecovcom  6590  ecovicom  6591  mapvalg  6606  pmvalg  6607  elpmg  6612  elmapssres  6621  pmss12g  6623  ixpconstg  6655  ener  6727  domtr  6733  f1imaeng  6740  fundmen  6754  xpcomco  6774  xpsnen2g  6777  xpdom2  6779  xpdom1g  6781  enen2  6789  domen2  6791  ssfilem  6823  diffitest  6835  fiintim  6876  fundmfibi  6886  cnvti  6966  djuex  6990  nnnninf  7072  ltsopi  7243  pitric  7244  pitri3or  7245  addcompig  7252  mulcompig  7254  ltapig  7261  ltmpig  7262  nnppipi  7266  addcomnqg  7304  addassnqg  7305  distrnqg  7310  recexnq  7313  nqtri3or  7319  ltmnqg  7324  lt2addnq  7327  lt2mulnq  7328  ltbtwnnqq  7338  prarloclemarch2  7342  enq0ref  7356  distrnq0  7382  mulcomnq0  7383  prcdnql  7407  prcunqu  7408  prarloclemlt  7416  genpassl  7447  genpassu  7448  nqprloc  7468  nqpru  7475  appdiv0nq  7487  addcomprg  7501  mulcomprg  7503  distrlem4prl  7507  distrlem4pru  7508  1idprl  7513  1idpru  7514  ltsopr  7519  recexprlemss1l  7558  recexprlemss1u  7559  gt0srpr  7671  mulcomsrg  7680  ltsosr  7687  aptisr  7702  mulextsr1  7704  map2psrprg  7728  axaddcom  7793  axltwlin  7948  axapti  7951  letri3  7961  eqlelt  7967  mul31  8011  cnegexlem3  8057  subval  8072  subcl  8079  pncan2  8087  pncan3  8088  npcan  8089  addsubeq4  8095  npncan3  8118  negsubdi2  8139  muladd  8264  subdi  8265  mulneg2  8276  mulsub  8281  ltleadd  8326  ltsubpos  8334  posdif  8335  addge01  8352  lesub0  8359  reapneg  8477  prodgt02  8730  prodge02  8732  ltdivmul  8753  lerec  8761  lediv2a  8772  le2msq  8778  msq11  8779  lbreu  8822  dfinfre  8833  creur  8836  creui  8837  cju  8838  nnmulcl  8860  nndivtr  8881  avgle1  9079  avgle2  9080  nn0nnaddcl  9127  zletric  9217  zrevaddcl  9223  znnsub  9224  znn0sub  9238  zdclt  9247  zextlt  9262  gtndiv  9265  prime  9269  peano5uzti  9278  uztrn2  9462  uztric  9466  uz11  9467  nn0pzuz  9504  indstr  9510  supinfneg  9512  infsupneg  9513  eluzdc  9527  qrevaddcl  9560  difrp  9606  xrltnsym  9707  xrltso  9710  xrlttri3  9711  xrletri3  9716  xleneg  9748  xaddcom  9772  xposdif  9793  ixxssixx  9813  iccid  9836  iooshf  9863  iccsupr  9877  iooneg  9899  iccneg  9900  fztri3or  9948  fzdcel  9949  fzn  9951  fzen  9952  fzass4  9971  fzrev  9993  fznn  9998  elfzp1b  10006  elfzm1b  10007  fz0fzdiffz0  10039  difelfznle  10044  fzon  10075  fzonmapblen  10096  eluzgtdifelfzo  10106  ubmelm1fzo  10135  subfzo0  10151  qletric  10153  ioo0  10169  ico0  10171  ioc0  10172  flqbi  10199  flqbi2  10200  flqzadd  10207  modfzo0difsn  10304  fzfig  10339  expcllem  10440  expap0  10459  mulbinom2  10544  expnbnd  10551  sq11ap  10595  hashfacen  10719  shftlem  10728  shftuz  10729  shftfvalg  10730  ovshftex  10731  shftfval  10733  shftval4  10740  shftval5  10741  2shfti  10743  mulreap  10776  sqrt11ap  10950  abs3dif  11017  abs2difabs  11020  maxabslemval  11120  maxle2  11124  maxclpr  11134  2zsupmax  11137  xrmaxiflemval  11159  xrmax2sup  11163  iooinsup  11186  climshftlemg  11211  fsumcnv  11346  explecnv  11414  geo2lim  11425  prodmodc  11487  fprodcnv  11534  demoivre  11681  demoivreALT  11682  nndivides  11705  0dvds  11719  muldvds1  11724  muldvds2  11725  dvdssubr  11746  dvdsadd2b  11747  odd2np1  11777  mulsucdiv2z  11789  ltoddhalfle  11797  ndvdssub  11834  gcdcom  11873  neggcd  11883  gcdabs2  11890  modgcd  11891  bezoutlemaz  11903  dfgcd2  11914  lcmcom  11957  neglcm  11968  lcmgcdeq  11976  coprmdvds  11985  qredeq  11989  divgcdcoprmex  11995  isprm3  12011  prmind2  12013  dvdsprm  12030  cncongrprm  12048  sqrt2irr  12053  hashgcdeq  12130  modprmn0modprm0  12147  coprimeprodsq  12148  pythagtriplem1  12156  pythagtriplem4  12159  eltg  12548  eltg2  12549  tgss  12559  tgss2  12575  basgen2  12577  bastop1  12579  opnneiss  12654  cnrest  12731  txss12  12762  hmeofvalg  12799  txswaphmeolem  12816  txswaphmeo  12817  blpnfctr  12935  metequiv  12991  metcnp3  13007  qtopbasss  13017  reopnap  13034  bl2ioo  13038  ioo2bl  13039  ioo2blex  13040  cncfval  13055  divccncfap  13073  addccncf  13082  expcncf  13088  dvexp  13171  dvef  13184  efle  13193  reapef  13195  ptolemy  13241  logleb  13292  uzdcinzz  13469  exmidsbthrlem  13690  triap  13697