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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simp1ll  1091  simp2ll  1095  simp3ll  1099  rmob  3145  ifnefals  3685  ifeqeqxdc  3687  prneimg  3899  exmid01  4335  pwntru  4336  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  poinxp  4844  mpteqb  5796  fvmptt  5797  fcof1  5989  acexmid  6084  fsuppeqg  6488  fvn0elsupp  6491  suppssdc  6500  suppssfvg  6503  dftpos4  6534  tfrlem3ag  6580  tfrlem3a  6581  tfrlemi1  6603  tfrexlem  6605  tfr1onlem3ag  6608  nntr2  6776  dcdifsnid  6777  qsel  6886  ecopovsymg  6908  ecopoverg  6910  th3qlem1  6911  mapss  6973  xpmapenlem  7149  findcard2  7193  findcard2s  7194  findcard2sd  7196  unfiin  7233  f1finf1o  7264  fidcenumlemrk  7271  fidcenumlemr  7272  fidcenum  7273  sbthlemi6  7279  sbthlemi8  7281  elfi2  7306  f1setfi  7317  2omap  7319  2omapfi  7321  supisolem  7349  enumct  7456  nninfninc  7464  ismkvnex  7496  exmidontriimlem4  7581  netap  7621  2omotaplemap  7624  cc2lem  7633  dfplpq2  7722  dfmpq2  7723  mulpipqqs  7741  distrnqg  7755  ltexnqq  7776  subhalfnqq  7782  prarloclemarch  7786  nnnq0lem1  7814  distrnq0  7827  npsspw  7839  prarloclemlo  7862  prarloclem3  7865  prarloclemcalc  7870  genplt2i  7878  distrlem1prl  7950  distrlem1pru  7951  distrlem4prl  7952  distrlem4pru  7953  ltprordil  7957  ltexprlemlol  7970  ltexprlemupu  7972  addextpr  7989  recexprlemopl  7993  recexprlemdisj  7998  recexprlem1ssl  8001  aptiprleml  8007  prsrlem1  8110  recexgt0sr  8141  addcnsr  8202  mulcnsr  8203  mulcnsrec  8211  axaddcl  8232  axmulcl  8234  axmulcom  8239  rereceu  8257  mpomulf  8317  ltntri  8456  cnegexlem1  8503  cnegex  8506  addsub4  8571  le2add  8774  lt2add  8775  lt2sub  8790  le2sub  8791  rereim  8917  apreim  8934  mulreim  8935  addext  8941  mulext  8945  receuap  9002  rec11ap  9043  rec11rap  9044  divdivdivap  9046  ddcanap  9059  divadddivap  9060  divsubdivap  9061  conjmulap  9062  rerecclap  9063  subrecap  9172  recgt0  9183  prodgt0gt0  9184  prodgt0  9185  prodge0  9187  ltmul12a  9193  lemul12a  9195  lemulge11  9199  lt2mul2div  9212  ltrec  9216  lerec  9217  lt2msq  9219  ltrec1  9221  le2msq  9234  msq11  9235  ledivp1  9236  mulle0r  9277  peano5uzti  9759  eluzuzle  9940  qreccl  10052  irraddap  10057  elpq  10060  xrltso  10209  z2ge  10239  xpncan  10284  xaddge0  10291  xle2add  10292  xleaddadd  10300  ixxss1  10317  ixxss2  10318  elioc2  10349  divelunit  10415  fzass4  10479  fzrev  10502  fzonmapblen  10610  elfzodifsumelfzo  10630  ssfzo12bi  10654  rebtwn2z  10700  qbtwnxr  10703  flaplt  10733  modqid  10801  modqcyc  10811  modqaddabs  10814  modqaddmod  10815  mulqaddmodid  10816  modqadd2mod  10826  modqltm1p1mod  10828  modqsubmod  10834  modqsubmodmod  10835  modqmulmod  10841  modqmulmodr  10842  modqsubdir  10845  frecuzrdgg  10868  nninfinf  10895  seq3val  10912  seqvalcd  10913  seq3feq  10932  seq3f1olemp  10967  seqfeq4g  10983  expp1  10998  expcl2lemap  11003  expnegzap  11025  expadd  11033  expmul  11036  leexp1a  11046  resq01  11110  expnlbnd  11117  nn0ltexp2  11163  nn0opth2  11178  bcval  11203  bcval5  11217  bcpasc  11220  hashunsng  11264  sseqn  11295  hashfibclem  11298  hashfibc  11299  hashf1lem2  11302  seq3coll  11310  iswrdiz  11327  sswrd  11329  ccatalpha  11397  ccatw2s1p1g  11429  swrdwrdsymbg  11452  swrdsb0eq  11453  ccatswrd  11458  pfxf  11470  pfxwrdsymbg  11478  wrd2ind  11511  swrdccatin2  11517  pfxccatin12lem2  11519  pfxccatin12lem3  11520  pfxccatin12  11521  pfxccat3  11522  swrdccat  11523  shftfvalg  11599  shftfval  11602  seq3shft  11619  caucvgrelemrec  11761  resqrexlemdecn  11794  sqrtmul  11817  sqrtdiv  11824  leabs  11856  absexpzap  11863  ltabs  11870  abslt  11871  absle  11872  abssubap0  11873  amgm2  11901  icodiamlt  11963  qdenre  11985  maxleim  11988  maxleastlt  11998  rexico  12004  zmaxcl  12007  minmax  12014  zmincl  12023  xrmaxleastlt  12041  xrminmax  12050  climuni  12078  cn1lem  12099  iserex  12124  iserle  12127  climserle  12130  climcau  12132  summodclem2a  12167  summodc  12169  isumss  12177  fisumss  12178  fsumadd  12192  isumadd  12217  fsum2dlemstep  12220  fsum2d  12221  fisum0diag2  12233  fsumabs  12251  isumsplit  12277  geolim  12297  geo2lim  12302  geoisum  12303  geoisumr  12304  geoisum1  12305  mertenslemub  12320  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  prodmodclem2  12363  prodmodc  12364  zproddc  12365  fprodseq  12369  fprodcl2lem  12391  fprod2dlemstep  12408  fprodle  12426  fprodmodd  12427  efcvgfsum  12453  eftlcl  12474  reeftlcl  12475  tanaddap  12525  zdvdsdc  12598  dvds2ln  12610  dvdsle  12630  divconjdvds  12635  dvdsext  12641  bitsfzo  12741  gcdsupex  12753  gcdsupcl  12754  bezoutlemmain  12794  bezoutlemaz  12799  bezoutlembi  12801  bezout  12807  gcdmultiplez  12817  dvdsmulgcd  12821  bezoutr  12828  bezoutr1  12829  lcmval  12860  lcmcllem  12864  ncoprmgcdne1b  12886  cncongr1  12900  isprm5  12940  prmdvdsexp  12946  sqrt2irr  12960  pwbdvdslemn  12963  nonsq  13006  powm2modprm  13054  pcmul  13103  pcqmul  13105  pcexp  13111  pcneg  13127  pcdvdstr  13129  pcprmpw2  13135  pcfac  13152  expnprm  13155  prmpwdvds  13157  mul4sq  13196  ballotfilem2  13280  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemsima  13311  ssnnctlemct  13389  infpn2  13399  isstruct2r  13415  setsfun  13439  setsfun0  13440  ismndd  13803  submnd0  13810  mhmf1o  13830  resmhm  13847  mhmco  13850  mhmima  13851  dfgrp2  13885  grprcan  13895  grplmulf1o  13932  grplactcnv  13960  mhmmnd  13972  mulgval  13978  mulgz  14006  mulgnn0dir  14008  mulgdir  14010  mulgneg2  14012  mhmmulg  14019  issubg4m  14049  nmzsubg  14066  ssnmz  14067  ghmmhmb  14110  resghm  14116  ghmpreima  14122  ghmnsgpreima  14125  ghmf1o  14131  resscntz  14160  cntzsgrpcl  14161  cntzsubm  14164  cntzsubg  14165  cntzmhm  14167  eqgabl  14218  gzsumconst  14227  pwssub  14300  rngpropd  14338  srglmhm  14381  srgrmhm  14382  isring  14388  ringadd2  14416  ringpropd  14427  ringlghm  14450  ringrghm  14451  oppr1g  14472  dvdsrex  14489  dvdsrtr  14492  issubrg  14613  unitrrg  14660  aprnzr  14683  opprdrng  14704  islmod  14711  islmodd  14713  lmodfopne  14747  lmodprop2d  14769  lssvacl  14786  lssvsubcl  14787  lssvscl  14796  islss3  14800  lsslss  14802  lss1d  14804  lsspropdg  14852  dflidl2rng  14902  expghmap  15026  mulgghm2  15027  znval  15055  znunit  15078  znrrg  15079  assapropd  15098  assamulgscmlem1  15125  assamulgscmlem2  15126  psrbaglesuppg  15141  mplvalcoe  15172  neissex  15357  tgrest  15361  ssrest  15374  restopn2  15375  cnco  15413  cnss1  15418  cnss2  15419  cnptopresti  15430  uptx  15466  txrest  15468  psmetres2  15525  xmetres2  15571  xblss2ps  15596  blhalf  15600  blssexps  15621  blssex  15622  blin2  15624  blbas  15625  bdmetval  15692  metcnpi  15707  metcnpi2  15708  qtopbas  15714  tgqioo  15747  cncfss  15775  mulc1cncf  15781  cncfmptid  15789  dedekindicc  15825  ivthdec  15836  cnplimcim  15859  cnplimclemle  15860  cnplimccntop  15862  limccnp2cntop  15869  dvfgg  15880  dvcj  15901  dvrecap  15905  dvmptfsum  15917  dveflem  15918  elply2  15927  ply1termlem  15934  plymullem1  15940  eflt  15967  ptolemy  16017  cos11  16046  logdivlt  16088  logdivle  16089  rpcxpmul2  16110  cxplt  16113  cxple  16114  cxplt3  16117  apcxp2  16136  rprelogbmul  16152  rprelogbdiv  16154  birthdaylem3  16188  pellexlem3  16192  efnnfsumcl  16200  sgmval  16213  sgmval2  16214  sgmf  16216  efchtqdvds  16226  sgmmul  16251  perfect  16262  bcmax  16266  bposlem1  16272  bpos  16281  lgsval2lem  16295  lgsdir2lem5  16317  2sqlem6  16405  umgrnloopv  16521  upgredg  16551  usgr1eop  16652  upgredginwlk  16763  wlkv0  16776  clwwlkccatlem  16807  pw1map  17191  pwtrufal  17193  nninfalllem1  17217  nninfsellemqall  17224  nnnninfex  17231  sbthom  17237  qdencn  17238  isomninnlem  17245  trirec0  17260  apdiff  17264  qdiff  17265  iswomninnlem  17266  ismkvnnlem  17269  ltlenmkv  17287