Theorem simpll 531

Description: Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)

Assertion

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

Proof of Theorem simpll

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ph -> ph )
2	1	ad2antrr 492	1 |- ( ( ( ph /\ ps ) /\ ch ) -> ph )

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:  simp1ll  1091  simp2ll  1095  simp3ll  1099  rmob  3145  ifnefals  3682  ifeqeqxdc  3684  prneimg  3894  exmid01  4330  pwntru  4331  ordtri2or2exmidlem  4668  onsucelsucexmidlem  4671  poinxp  4839  mpteqb  5790  fvmptt  5791  fcof1  5979  acexmid  6074  fsuppeqg  6478  fvn0elsupp  6481  suppssdc  6490  suppssfvg  6493  dftpos4  6524  tfrlem3ag  6570  tfrlem3a  6571  tfrlemi1  6593  tfrexlem  6595  tfr1onlem3ag  6598  nntr2  6766  dcdifsnid  6767  qsel  6876  ecopovsymg  6898  ecopoverg  6900  th3qlem1  6901  mapss  6963  xpmapenlem  7139  findcard2  7183  findcard2s  7184  findcard2sd  7186  unfiin  7223  f1finf1o  7254  fidcenumlemrk  7261  fidcenumlemr  7262  fidcenum  7263  sbthlemi6  7269  sbthlemi8  7271  elfi2  7296  f1setfi  7307  2omap  7308  2omapfi  7310  supisolem  7338  enumct  7445  nninfninc  7453  ismkvnex  7485  exmidontriimlem4  7570  netap  7610  2omotaplemap  7613  cc2lem  7622  dfplpq2  7711  dfmpq2  7712  mulpipqqs  7730  distrnqg  7744  ltexnqq  7765  subhalfnqq  7771  prarloclemarch  7775  nnnq0lem1  7803  distrnq0  7816  npsspw  7828  prarloclemlo  7851  prarloclem3  7854  prarloclemcalc  7859  genplt2i  7867  distrlem1prl  7939  distrlem1pru  7940  distrlem4prl  7941  distrlem4pru  7942  ltprordil  7946  ltexprlemlol  7959  ltexprlemupu  7961  addextpr  7978  recexprlemopl  7982  recexprlemdisj  7987  recexprlem1ssl  7990  aptiprleml  7996  prsrlem1  8099  recexgt0sr  8130  addcnsr  8191  mulcnsr  8192  mulcnsrec  8200  axaddcl  8221  axmulcl  8223  axmulcom  8228  rereceu  8246  mpomulf  8306  ltntri  8444  cnegexlem1  8491  cnegex  8494  addsub4  8559  le2add  8762  lt2add  8763  lt2sub  8778  le2sub  8779  rereim  8904  apreim  8921  mulreim  8922  addext  8928  mulext  8932  receuap  8989  rec11ap  9030  rec11rap  9031  divdivdivap  9033  ddcanap  9046  divadddivap  9047  divsubdivap  9048  conjmulap  9049  rerecclap  9050  subrecap  9159  recgt0  9170  prodgt0gt0  9171  prodgt0  9172  prodge0  9174  ltmul12a  9180  lemul12a  9182  lemulge11  9186  lt2mul2div  9199  ltrec  9203  lerec  9204  lt2msq  9206  ltrec1  9208  le2msq  9221  msq11  9222  ledivp1  9223  mulle0r  9264  peano5uzti  9733  eluzuzle  9909  qreccl  10021  elpq  10028  xrltso  10177  z2ge  10207  xpncan  10252  xaddge0  10259  xle2add  10260  xleaddadd  10268  ixxss1  10285  ixxss2  10286  elioc2  10317  divelunit  10383  fzass4  10446  fzrev  10469  fzonmapblen  10577  elfzodifsumelfzo  10597  ssfzo12bi  10621  rebtwn2z  10667  qbtwnxr  10670  modqid  10764  modqcyc  10774  modqaddabs  10777  modqaddmod  10778  mulqaddmodid  10779  modqadd2mod  10789  modqltm1p1mod  10791  modqsubmod  10797  modqsubmodmod  10798  modqmulmod  10804  modqmulmodr  10805  modqsubdir  10808  frecuzrdgg  10831  nninfinf  10858  seq3val  10875  seqvalcd  10876  seq3feq  10895  seq3f1olemp  10930  seqfeq4g  10946  expp1  10961  expcl2lemap  10966  expnegzap  10988  expadd  10996  expmul  10999  leexp1a  11009  resq01  11073  expnlbnd  11080  nn0ltexp2  11125  nn0opth2  11140  bcval  11165  bcval5  11179  bcpasc  11182  hashunsng  11226  sseqn  11257  hashfibclem  11260  hashfibc  11261  hashf1lem2  11264  seq3coll  11272  iswrdiz  11289  sswrd  11291  ccatalpha  11359  ccatw2s1p1g  11391  swrdwrdsymbg  11414  swrdsb0eq  11415  ccatswrd  11420  pfxf  11432  pfxwrdsymbg  11440  wrd2ind  11473  swrdccatin2  11479  pfxccatin12lem2  11481  pfxccatin12lem3  11482  pfxccatin12  11483  pfxccat3  11484  swrdccat  11485  shftfvalg  11561  shftfval  11564  seq3shft  11581  caucvgrelemrec  11723  resqrexlemdecn  11756  sqrtmul  11779  sqrtdiv  11786  leabs  11818  absexpzap  11824  ltabs  11831  abslt  11832  absle  11833  abssubap0  11834  amgm2  11862  icodiamlt  11924  qdenre  11946  maxleim  11949  maxleastlt  11959  rexico  11965  zmaxcl  11968  minmax  11974  xrmaxleastlt  12000  xrminmax  12009  climuni  12037  cn1lem  12058  iserex  12083  iserle  12086  climserle  12089  climcau  12091  summodclem2a  12126  summodc  12128  isumss  12136  fisumss  12137  fsumadd  12151  isumadd  12176  fsum2dlemstep  12179  fsum2d  12180  fisum0diag2  12192  fsumabs  12210  isumsplit  12236  geolim  12256  geo2lim  12261  geoisum  12262  geoisumr  12263  geoisum1  12264  mertenslemub  12279  mertenslemi1  12280  mertenslem2  12281  mertensabs  12282  prodmodclem2  12322  prodmodc  12323  zproddc  12324  fprodseq  12328  fprodcl2lem  12350  fprod2dlemstep  12367  fprodle  12385  fprodmodd  12386  efcvgfsum  12412  eftlcl  12433  reeftlcl  12434  tanaddap  12484  zdvdsdc  12557  dvds2ln  12569  dvdsle  12589  divconjdvds  12594  dvdsext  12600  bitsfzo  12700  gcdsupex  12712  gcdsupcl  12713  bezoutlemmain  12753  bezoutlemaz  12758  bezoutlembi  12760  bezout  12766  gcdmultiplez  12776  dvdsmulgcd  12780  bezoutr  12787  bezoutr1  12788  lcmval  12819  lcmcllem  12823  ncoprmgcdne1b  12845  cncongr1  12859  isprm5  12898  prmdvdsexp  12904  sqrt2irr  12918  pw2dvdslemn  12921  pw2dvdseu  12924  nonsq  12963  powm2modprm  13009  pcmul  13058  pcqmul  13060  pcexp  13066  pcneg  13082  pcdvdstr  13084  pcprmpw2  13090  pcfac  13107  expnprm  13110  prmpwdvds  13112  mul4sq  13151  ballotfilem2  13206  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemsima  13237  ssnnctlemct  13315  infpn2  13325  isstruct2r  13341  setsfun  13365  setsfun0  13366  ismndd  13727  submnd0  13734  mhmf1o  13754  resmhm  13771  mhmco  13774  mhmima  13775  dfgrp2  13809  grprcan  13819  grplmulf1o  13856  grplactcnv  13884  mhmmnd  13896  mulgval  13902  mulgz  13930  mulgnn0dir  13932  mulgdir  13934  mulgneg2  13936  mhmmulg  13943  issubg4m  13973  nmzsubg  13990  ssnmz  13991  ghmmhmb  14034  resghm  14040  ghmpreima  14046  ghmnsgpreima  14049  ghmf1o  14055  eqgabl  14111  gzsumconst  14120  pwssub  14193  rngpropd  14229  srglmhm  14271  srgrmhm  14272  isring  14278  ringadd2  14305  ringpropd  14316  ringlghm  14339  ringrghm  14340  oppr1g  14361  dvdsrex  14378  dvdsrtr  14381  issubrg  14502  unitrrg  14549  aprnzr  14572  opprdrng  14593  islmod  14600  islmodd  14602  lmodfopne  14635  lmodprop2d  14657  lssvacl  14674  lssvsubcl  14675  lssvscl  14684  islss3  14688  lsslss  14690  lss1d  14692  lsspropdg  14740  dflidl2rng  14790  expghmap  14914  mulgghm2  14915  znval  14943  znunit  14966  znrrg  14967  psrbaglesuppg  14980  mplvalcoe  15004  neissex  15189  tgrest  15193  ssrest  15206  restopn2  15207  cnco  15245  cnss1  15250  cnss2  15251  cnptopresti  15262  uptx  15298  txrest  15300  psmetres2  15357  xmetres2  15403  xblss2ps  15428  blhalf  15432  blssexps  15453  blssex  15454  blin2  15456  blbas  15457  bdmetval  15524  metcnpi  15539  metcnpi2  15540  qtopbas  15546  tgqioo  15579  cncfss  15607  mulc1cncf  15613  cncfmptid  15621  dedekindicc  15657  ivthdec  15668  cnplimcim  15691  cnplimclemle  15692  cnplimccntop  15694  limccnp2cntop  15701  dvfgg  15712  dvcj  15733  dvrecap  15737  dvmptfsum  15749  dveflem  15750  elply2  15759  ply1termlem  15766  plymullem1  15772  eflt  15799  ptolemy  15848  cos11  15877  rpcxpmul2  15938  cxplt  15941  cxple  15942  cxplt3  15945  apcxp2  15964  rprelogbmul  15980  rprelogbdiv  15982  pellexlem3  16007  sgmval  16011  sgmval2  16012  sgmf  16014  sgmmul  16024  perfect  16029  lgsval2lem  16043  lgsdir2lem5  16065  2sqlem6  16153  umgrnloopv  16269  upgredg  16299  usgr1eop  16400  upgredginwlk  16511  wlkv0  16524  clwwlkccatlem  16555  pw1map  16939  pwtrufal  16941  nninfalllem1  16956  nninfsellemqall  16963  nnnninfex  16970  sbthom  16976  qdencn  16977  isomninnlem  16984  trirec0  16998  apdiff  17002  qdiff  17003  iswomninnlem  17004  ismkvnnlem  17007  ltlenmkv  17025