Theorem ancoms 268

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  adantl  277  syl2anr  290  anim12ci  339  sylan9bbr  463  anabss4  577  anabsi7  581  anabsi8  582  im2anan9r  599  bi2anan9r  607  syl3anr2  1291  mp3anr1  1334  mp3anr2  1335  mp3anr3  1336  stoic1b  1428  eu5  2073  2exeu  2118  eqeqan12rd  2194  sylan9eqr  2232  r19.29vva  2622  morex  2922  sylan9ssr  3170  riinm  3960  breqan12rd  4021  elnn  4606  soinxp  4697  seinxp  4698  brelrng  4859  dminss  5044  imainss  5045  funsng  5263  funcnvuni  5286  f1co  5434  f1ocnv  5475  fun11iun  5483  funimass4  5567  fndmdifcom  5623  fsn2  5691  fvtp2g  5726  fvtp3g  5727  fvtp2  5729  fvtp3  5730  acexmid  5874  oveqan12rd  5895  cofunex2g  6111  brtposg  6255  tposoprab  6281  smores3  6294  smores2  6295  smoel  6301  tfri3  6368  rdgtfr  6375  rdgruledefgg  6376  omcl  6462  oeicl  6463  nnmsucr  6489  nnmcom  6490  nndir  6491  nnaordi  6509  nnaordr  6511  nnaword  6512  nnmordi  6517  nnaordex  6529  nnm00  6531  ersym  6547  elecg  6573  riinerm  6608  ecopovsym  6631  ecopovsymg  6634  ecovcom  6642  ecovicom  6643  mapvalg  6658  pmvalg  6659  elpmg  6664  elmapssres  6673  pmss12g  6675  ixpconstg  6707  ener  6779  domtr  6785  f1imaeng  6792  fundmen  6806  xpcomco  6826  xpsnen2g  6829  xpdom2  6831  xpdom1g  6833  enen2  6841  domen2  6843  ssfilem  6875  diffitest  6887  fiintim  6928  fundmfibi  6938  cnvti  7018  djuex  7042  nnnninf  7124  netap  7253  2omotaplemap  7256  ltsopi  7319  pitric  7320  pitri3or  7321  addcompig  7328  mulcompig  7330  ltapig  7337  ltmpig  7338  nnppipi  7342  addcomnqg  7380  addassnqg  7381  distrnqg  7386  recexnq  7389  nqtri3or  7395  ltmnqg  7400  lt2addnq  7403  lt2mulnq  7404  ltbtwnnqq  7414  prarloclemarch2  7418  enq0ref  7432  distrnq0  7458  mulcomnq0  7459  prcdnql  7483  prcunqu  7484  prarloclemlt  7492  genpassl  7523  genpassu  7524  nqprloc  7544  nqpru  7551  appdiv0nq  7563  addcomprg  7577  mulcomprg  7579  distrlem4prl  7583  distrlem4pru  7584  1idprl  7589  1idpru  7590  ltsopr  7595  recexprlemss1l  7634  recexprlemss1u  7635  gt0srpr  7747  mulcomsrg  7756  ltsosr  7763  aptisr  7778  mulextsr1  7780  map2psrprg  7804  axaddcom  7869  axltwlin  8025  axapti  8028  letri3  8038  eqlelt  8044  mul31  8088  cnegexlem3  8134  subval  8149  subcl  8156  pncan2  8164  pncan3  8165  npcan  8166  addsubeq4  8172  npncan3  8195  negsubdi2  8216  muladd  8341  subdi  8342  mulneg2  8353  mulsub  8358  ltleadd  8403  ltsubpos  8411  posdif  8412  addge01  8429  lesub0  8436  reapneg  8554  prodgt02  8810  prodge02  8812  ltdivmul  8833  lerec  8841  lediv2a  8852  le2msq  8858  msq11  8859  lbreu  8902  dfinfre  8913  creur  8916  creui  8917  cju  8918  nnmulcl  8940  nndivtr  8961  avgle1  9159  avgle2  9160  nn0nnaddcl  9207  zletric  9297  zrevaddcl  9303  znnsub  9304  znn0sub  9318  ltsubnn0  9320  zdclt  9330  zextlt  9345  gtndiv  9348  prime  9352  peano5uzti  9361  uztrn2  9545  uztric  9549  uz11  9550  nn0pzuz  9587  indstr  9593  supinfneg  9595  infsupneg  9596  eluzdc  9610  qrevaddcl  9644  difrp  9692  xrltnsym  9793  xrltso  9796  xrlttri3  9797  xrletri3  9804  xleneg  9837  xaddcom  9861  xposdif  9882  ixxssixx  9902  iccid  9925  iooshf  9952  iccsupr  9966  iooneg  9988  iccneg  9989  fztri3or  10039  fzdcel  10040  fzn  10042  fzen  10043  fzass4  10062  fzrev  10084  fznn  10089  elfzp1b  10097  elfzm1b  10098  fz0fzdiffz0  10130  difelfznle  10135  fzon  10166  fzonmapblen  10187  eluzgtdifelfzo  10197  ubmelm1fzo  10226  subfzo0  10242  qletric  10244  ioo0  10260  ico0  10262  ioc0  10263  flqbi  10290  flqbi2  10291  flqzadd  10298  modfzo0difsn  10395  fzfig  10430  expcllem  10531  expap0  10550  mulbinom2  10637  expnbnd  10644  sq11ap  10688  hashfacen  10816  shftlem  10825  shftuz  10826  shftfvalg  10827  ovshftex  10828  shftfval  10830  shftval4  10837  shftval5  10838  2shfti  10840  mulreap  10873  sqrt11ap  11047  abs3dif  11114  abs2difabs  11117  maxabslemval  11217  maxle2  11221  maxclpr  11231  2zsupmax  11234  mingeb  11250  2zinfmin  11251  xrmaxiflemval  11258  xrmax2sup  11262  iooinsup  11285  climshftlemg  11310  fsumcnv  11445  explecnv  11513  geo2lim  11524  prodmodc  11586  fprodcnv  11633  demoivre  11780  demoivreALT  11781  nndivides  11804  0dvds  11818  muldvds1  11823  muldvds2  11824  dvdssubr  11846  dvdsadd2b  11847  odd2np1  11878  mulsucdiv2z  11890  ltoddhalfle  11898  ndvdssub  11935  gcdcom  11974  neggcd  11984  gcdabs2  11991  modgcd  11992  bezoutlemaz  12004  dfgcd2  12015  lcmcom  12064  neglcm  12075  lcmgcdeq  12083  coprmdvds  12092  qredeq  12096  divgcdcoprmex  12102  isprm3  12118  prmind2  12120  dvdsprm  12137  cncongrprm  12157  sqrt2irr  12162  hashgcdeq  12239  modprmn0modprm0  12256  coprimeprodsq  12257  pythagtriplem1  12265  pythagtriplem4  12268  pc2dvds  12329  pc11  12330  pcz  12331  pcprod  12344  prmunb  12360  1arithlem2  12362  1arithlem3  12363  1arith  12365  ptex  12713  issubmnd  12843  submcl  12870  grpinvsub  12952  dfgrp3mlem  12968  mgpress  13141  srgmulgass  13172  rmodislmodlem  13440  rmodislmod  13441  cnfldexp  13474  dvdsrzring  13496  eltg  13555  eltg2  13556  tgss  13566  tgss2  13582  basgen2  13584  bastop1  13586  opnneiss  13661  cnrest  13738  txss12  13769  hmeofvalg  13806  txswaphmeolem  13823  txswaphmeo  13824  blpnfctr  13942  metequiv  13998  metcnp3  14014  qtopbasss  14024  reopnap  14041  bl2ioo  14045  ioo2bl  14046  ioo2blex  14047  cncfval  14062  divccncfap  14080  addccncf  14089  expcncf  14095  dvexp  14178  dvef  14191  efle  14200  reapef  14202  ptolemy  14248  logleb  14299  lgsprme0  14446  2lgsoddprmlem2  14457  uzdcinzz  14553  exmidsbthrlem  14773  triap  14780