Theorem simpll 527

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 488	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  1062  simp2ll  1066  simp3ll  1070  rmob  3090  ifnefals  3613  prneimg  3814  exmid01  4241  pwntru  4242  ordtri2or2exmidlem  4572  onsucelsucexmidlem  4575  poinxp  4742  mpteqb  5664  fvmptt  5665  fcof1  5842  acexmid  5933  dftpos4  6339  tfrlem3ag  6385  tfrlem3a  6386  tfrlemi1  6408  tfrexlem  6410  tfr1onlem3ag  6413  nntr2  6579  dcdifsnid  6580  qsel  6689  ecopovsymg  6711  ecopoverg  6713  th3qlem1  6714  mapss  6768  xpmapenlem  6928  findcard2  6968  findcard2s  6969  findcard2sd  6971  unfiin  7005  f1finf1o  7031  fidcenumlemrk  7038  fidcenumlemr  7039  fidcenum  7040  sbthlemi6  7046  sbthlemi8  7048  elfi2  7056  supisolem  7092  enumct  7199  nninfninc  7207  ismkvnex  7239  exmidontriimlem4  7318  netap  7348  2omotaplemap  7351  cc2lem  7360  dfplpq2  7449  dfmpq2  7450  mulpipqqs  7468  distrnqg  7482  ltexnqq  7503  subhalfnqq  7509  prarloclemarch  7513  nnnq0lem1  7541  distrnq0  7554  npsspw  7566  prarloclemlo  7589  prarloclem3  7592  prarloclemcalc  7597  genplt2i  7605  distrlem1prl  7677  distrlem1pru  7678  distrlem4prl  7679  distrlem4pru  7680  ltprordil  7684  ltexprlemlol  7697  ltexprlemupu  7699  addextpr  7716  recexprlemopl  7720  recexprlemdisj  7725  recexprlem1ssl  7728  aptiprleml  7734  prsrlem1  7837  recexgt0sr  7868  addcnsr  7929  mulcnsr  7930  mulcnsrec  7938  axaddcl  7959  axmulcl  7961  axmulcom  7966  rereceu  7984  mpomulf  8044  ltntri  8182  cnegexlem1  8229  cnegex  8232  addsub4  8297  le2add  8499  lt2add  8500  lt2sub  8515  le2sub  8516  rereim  8641  apreim  8658  mulreim  8659  addext  8665  mulext  8669  receuap  8724  rec11ap  8765  rec11rap  8766  divdivdivap  8768  ddcanap  8781  divadddivap  8782  divsubdivap  8783  conjmulap  8784  rerecclap  8785  subrecap  8894  recgt0  8905  prodgt0gt0  8906  prodgt0  8907  prodge0  8909  ltmul12a  8915  lemul12a  8917  lemulge11  8921  lt2mul2div  8934  ltrec  8938  lerec  8939  lt2msq  8941  ltrec1  8943  le2msq  8956  msq11  8957  ledivp1  8958  mulle0r  8999  peano5uzti  9463  eluzuzle  9638  qreccl  9745  elpq  9752  xrltso  9900  z2ge  9930  xpncan  9975  xaddge0  9982  xle2add  9983  xleaddadd  9991  ixxss1  10008  ixxss2  10009  elioc2  10040  divelunit  10106  fzass4  10166  fzrev  10188  fzonmapblen  10292  elfzodifsumelfzo  10311  ssfzo12bi  10335  rebtwn2z  10378  qbtwnxr  10381  modqid  10475  modqcyc  10485  modqaddabs  10488  modqaddmod  10489  mulqaddmodid  10490  modqadd2mod  10500  modqltm1p1mod  10502  modqsubmod  10508  modqsubmodmod  10509  modqmulmod  10515  modqmulmodr  10516  modqsubdir  10519  frecuzrdgg  10542  nninfinf  10569  seq3val  10586  seqvalcd  10587  seq3feq  10606  seq3f1olemp  10641  seqfeq4g  10657  expp1  10672  expcl2lemap  10677  expnegzap  10699  expadd  10707  expmul  10710  leexp1a  10720  expnlbnd  10790  nn0ltexp2  10835  nn0opth2  10850  bcval  10875  bcval5  10889  bcpasc  10892  hashunsng  10933  seq3coll  10968  iswrdiz  10976  sswrd  10978  shftfvalg  11048  shftfval  11051  seq3shft  11068  caucvgrelemrec  11209  resqrexlemdecn  11242  sqrtmul  11265  sqrtdiv  11272  leabs  11304  absexpzap  11310  ltabs  11317  abslt  11318  absle  11319  abssubap0  11320  amgm2  11348  icodiamlt  11410  qdenre  11432  maxleim  11435  maxleastlt  11445  rexico  11451  zmaxcl  11454  minmax  11460  xrmaxleastlt  11486  xrminmax  11495  climuni  11523  cn1lem  11544  iserex  11569  iserle  11572  climserle  11575  climcau  11577  summodclem2a  11611  summodc  11613  isumss  11621  fisumss  11622  fsumadd  11636  isumadd  11661  fsum2dlemstep  11664  fsum2d  11665  fisum0diag2  11677  fsumabs  11695  isumsplit  11721  geolim  11741  geo2lim  11746  geoisum  11747  geoisumr  11748  geoisum1  11749  mertenslemub  11764  mertenslemi1  11765  mertenslem2  11766  mertensabs  11767  prodmodclem2  11807  prodmodc  11808  zproddc  11809  fprodseq  11813  fprodcl2lem  11835  fprod2dlemstep  11852  fprodle  11870  fprodmodd  11871  efcvgfsum  11897  eftlcl  11918  reeftlcl  11919  tanaddap  11969  zdvdsdc  12042  dvds2ln  12054  dvdsle  12074  divconjdvds  12079  dvdsext  12085  bitsfzo  12185  gcdsupex  12197  gcdsupcl  12198  bezoutlemmain  12238  bezoutlemaz  12243  bezoutlembi  12245  bezout  12251  gcdmultiplez  12261  dvdsmulgcd  12265  bezoutr  12272  bezoutr1  12273  lcmval  12304  lcmcllem  12308  ncoprmgcdne1b  12330  cncongr1  12344  isprm5  12383  prmdvdsexp  12389  sqrt2irr  12403  pw2dvdslemn  12406  pw2dvdseu  12409  nonsq  12448  powm2modprm  12494  pcmul  12543  pcqmul  12545  pcexp  12551  pcneg  12567  pcdvdstr  12569  pcprmpw2  12575  pcfac  12592  expnprm  12595  prmpwdvds  12597  mul4sq  12636  ssnnctlemct  12736  infpn2  12746  isstruct2r  12762  setsfun  12786  setsfun0  12787  ismndd  13187  submnd0  13194  mhmf1o  13220  resmhm  13237  mhmco  13240  mhmima  13241  dfgrp2  13277  grprcan  13287  grplmulf1o  13324  grplactcnv  13352  pwssub  13363  mhmmnd  13370  mulgval  13376  mulgz  13404  mulgnn0dir  13406  mulgdir  13408  mulgneg2  13410  mhmmulg  13417  issubg4m  13447  nmzsubg  13464  ssnmz  13465  ghmmhmb  13508  resghm  13514  ghmpreima  13520  ghmnsgpreima  13523  ghmf1o  13529  eqgabl  13584  gsumfzconst  13595  rngpropd  13635  srglmhm  13673  srgrmhm  13674  isring  13680  ringadd2  13707  ringpropd  13718  ringlghm  13741  ringrghm  13742  oppr1g  13762  dvdsrex  13778  dvdsrtr  13781  issubrg  13901  unitrrg  13947  islmod  13971  islmodd  13973  lmodfopne  14006  lmodprop2d  14028  lssvacl  14045  lssvsubcl  14046  lssvscl  14055  islss3  14059  lsslss  14061  lss1d  14063  lsspropdg  14111  dflidl2rng  14161  gsumfzfsumlemm  14267  expghmap  14287  mulgghm2  14288  znval  14316  znunit  14339  znrrg  14340  psrbaglesuppg  14352  mplvalcoe  14370  neissex  14555  tgrest  14559  ssrest  14572  restopn2  14573  cnco  14611  cnss1  14616  cnss2  14617  cnptopresti  14628  uptx  14664  txrest  14666  psmetres2  14723  xmetres2  14769  xblss2ps  14794  blhalf  14798  blssexps  14819  blssex  14820  blin2  14822  blbas  14823  bdmetval  14890  metcnpi  14905  metcnpi2  14906  qtopbas  14912  tgqioo  14945  cncfss  14973  mulc1cncf  14979  cncfmptid  14987  dedekindicc  15023  ivthdec  15034  cnplimcim  15057  cnplimclemle  15058  cnplimccntop  15060  limccnp2cntop  15067  dvfgg  15078  dvcj  15099  dvrecap  15103  dvmptfsum  15115  dveflem  15116  elply2  15125  ply1termlem  15132  plymullem1  15138  eflt  15165  ptolemy  15214  cos11  15243  rpcxpmul2  15303  cxplt  15306  cxple  15307  cxplt3  15310  apcxp2  15329  rprelogbmul  15345  rprelogbdiv  15347  sgmval  15373  sgmval2  15374  sgmf  15376  sgmmul  15386  perfect  15391  lgsval2lem  15405  lgsdir2lem5  15427  2sqlem6  15515  2omap  15796  pwtrufal  15798  nninfalllem1  15809  nninfsellemqall  15816  nnnninfex  15823  sbthom  15829  qdencn  15830  isomninnlem  15833  trirec0  15847  apdiff  15851  iswomninnlem  15852  ismkvnnlem  15855  ltlenmkv  15873