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  3079  ifnefals  3600  prneimg  3801  exmid01  4228  pwntru  4229  ordtri2or2exmidlem  4559  onsucelsucexmidlem  4562  poinxp  4729  mpteqb  5649  fvmptt  5650  fcof1  5827  acexmid  5918  dftpos4  6318  tfrlem3ag  6364  tfrlem3a  6365  tfrlemi1  6387  tfrexlem  6389  tfr1onlem3ag  6392  nntr2  6558  dcdifsnid  6559  qsel  6668  ecopovsymg  6690  ecopoverg  6692  th3qlem1  6693  mapss  6747  xpmapenlem  6907  findcard2  6947  findcard2s  6948  findcard2sd  6950  unfiin  6984  f1finf1o  7008  fidcenumlemrk  7015  fidcenumlemr  7016  fidcenum  7017  sbthlemi6  7023  sbthlemi8  7025  elfi2  7033  supisolem  7069  enumct  7176  nninfninc  7184  ismkvnex  7216  exmidontriimlem4  7286  netap  7316  2omotaplemap  7319  cc2lem  7328  dfplpq2  7416  dfmpq2  7417  mulpipqqs  7435  distrnqg  7449  ltexnqq  7470  subhalfnqq  7476  prarloclemarch  7480  nnnq0lem1  7508  distrnq0  7521  npsspw  7533  prarloclemlo  7556  prarloclem3  7559  prarloclemcalc  7564  genplt2i  7572  distrlem1prl  7644  distrlem1pru  7645  distrlem4prl  7646  distrlem4pru  7647  ltprordil  7651  ltexprlemlol  7664  ltexprlemupu  7666  addextpr  7683  recexprlemopl  7687  recexprlemdisj  7692  recexprlem1ssl  7695  aptiprleml  7701  prsrlem1  7804  recexgt0sr  7835  addcnsr  7896  mulcnsr  7897  mulcnsrec  7905  axaddcl  7926  axmulcl  7928  axmulcom  7933  rereceu  7951  mpomulf  8011  ltntri  8149  cnegexlem1  8196  cnegex  8199  addsub4  8264  le2add  8465  lt2add  8466  lt2sub  8481  le2sub  8482  rereim  8607  apreim  8624  mulreim  8625  addext  8631  mulext  8635  receuap  8690  rec11ap  8731  rec11rap  8732  divdivdivap  8734  ddcanap  8747  divadddivap  8748  divsubdivap  8749  conjmulap  8750  rerecclap  8751  subrecap  8860  recgt0  8871  prodgt0gt0  8872  prodgt0  8873  prodge0  8875  ltmul12a  8881  lemul12a  8883  lemulge11  8887  lt2mul2div  8900  ltrec  8904  lerec  8905  lt2msq  8907  ltrec1  8909  le2msq  8922  msq11  8923  ledivp1  8924  mulle0r  8965  peano5uzti  9428  eluzuzle  9603  qreccl  9710  elpq  9717  xrltso  9865  z2ge  9895  xpncan  9940  xaddge0  9947  xle2add  9948  xleaddadd  9956  ixxss1  9973  ixxss2  9974  elioc2  10005  divelunit  10071  fzass4  10131  fzrev  10153  fzonmapblen  10257  elfzodifsumelfzo  10271  ssfzo12bi  10295  rebtwn2z  10326  qbtwnxr  10329  modqid  10423  modqcyc  10433  modqaddabs  10436  modqaddmod  10437  mulqaddmodid  10438  modqadd2mod  10448  modqltm1p1mod  10450  modqsubmod  10456  modqsubmodmod  10457  modqmulmod  10463  modqmulmodr  10464  modqsubdir  10467  frecuzrdgg  10490  nninfinf  10517  seq3val  10534  seqvalcd  10535  seq3feq  10554  seq3f1olemp  10589  seqfeq4g  10605  expp1  10620  expcl2lemap  10625  expnegzap  10647  expadd  10655  expmul  10658  leexp1a  10668  expnlbnd  10738  nn0ltexp2  10783  nn0opth2  10798  bcval  10823  bcval5  10837  bcpasc  10840  hashunsng  10881  seq3coll  10916  iswrdiz  10924  sswrd  10926  shftfvalg  10965  shftfval  10968  seq3shft  10985  caucvgrelemrec  11126  resqrexlemdecn  11159  sqrtmul  11182  sqrtdiv  11189  leabs  11221  absexpzap  11227  ltabs  11234  abslt  11235  absle  11236  abssubap0  11237  amgm2  11265  icodiamlt  11327  qdenre  11349  maxleim  11352  maxleastlt  11362  rexico  11368  zmaxcl  11371  minmax  11376  xrmaxleastlt  11402  xrminmax  11411  climuni  11439  cn1lem  11460  iserex  11485  iserle  11488  climserle  11491  climcau  11493  summodclem2a  11527  summodc  11529  isumss  11537  fisumss  11538  fsumadd  11552  isumadd  11577  fsum2dlemstep  11580  fsum2d  11581  fisum0diag2  11593  fsumabs  11611  isumsplit  11637  geolim  11657  geo2lim  11662  geoisum  11663  geoisumr  11664  geoisum1  11665  mertenslemub  11680  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  prodmodclem2  11723  prodmodc  11724  zproddc  11725  fprodseq  11729  fprodcl2lem  11751  fprod2dlemstep  11768  fprodle  11786  fprodmodd  11787  efcvgfsum  11813  eftlcl  11834  reeftlcl  11835  tanaddap  11885  zdvdsdc  11958  dvds2ln  11970  dvdsle  11989  divconjdvds  11994  dvdsext  12000  gcdsupex  12097  gcdsupcl  12098  bezoutlemmain  12138  bezoutlemaz  12143  bezoutlembi  12145  bezout  12151  gcdmultiplez  12161  dvdsmulgcd  12165  bezoutr  12172  bezoutr1  12173  lcmval  12204  lcmcllem  12208  ncoprmgcdne1b  12230  cncongr1  12244  isprm5  12283  prmdvdsexp  12289  sqrt2irr  12303  pw2dvdslemn  12306  pw2dvdseu  12309  nonsq  12348  powm2modprm  12393  pcmul  12442  pcqmul  12444  pcexp  12450  pcneg  12466  pcdvdstr  12468  pcprmpw2  12474  pcfac  12491  expnprm  12494  prmpwdvds  12496  mul4sq  12535  ssnnctlemct  12606  infpn2  12616  isstruct2r  12632  setsfun  12656  setsfun0  12657  ismndd  13021  submnd0  13028  mhmf1o  13045  resmhm  13062  mhmco  13065  mhmima  13066  dfgrp2  13102  grprcan  13112  grplmulf1o  13149  grplactcnv  13177  mhmmnd  13189  mulgval  13195  mulgz  13223  mulgnn0dir  13225  mulgdir  13227  mulgneg2  13229  mhmmulg  13236  issubg4m  13266  nmzsubg  13283  ssnmz  13284  ghmmhmb  13327  resghm  13333  ghmpreima  13339  ghmnsgpreima  13342  ghmf1o  13348  eqgabl  13403  gsumfzconst  13414  rngpropd  13454  srglmhm  13492  srgrmhm  13493  isring  13499  ringadd2  13526  ringpropd  13537  ringlghm  13560  ringrghm  13561  oppr1g  13581  dvdsrex  13597  dvdsrtr  13600  issubrg  13720  unitrrg  13766  islmod  13790  islmodd  13792  lmodfopne  13825  lmodprop2d  13847  lssvacl  13864  lssvsubcl  13865  lssvscl  13874  islss3  13878  lsslss  13880  lss1d  13882  lsspropdg  13930  dflidl2rng  13980  gsumfzfsumlemm  14086  expghmap  14106  mulgghm2  14107  znval  14135  znunit  14158  znrrg  14159  psrbaglesuppg  14169  neissex  14344  tgrest  14348  ssrest  14361  restopn2  14362  cnco  14400  cnss1  14405  cnss2  14406  cnptopresti  14417  uptx  14453  txrest  14455  psmetres2  14512  xmetres2  14558  xblss2ps  14583  blhalf  14587  blssexps  14608  blssex  14609  blin2  14611  blbas  14612  bdmetval  14679  metcnpi  14694  metcnpi2  14695  qtopbas  14701  tgqioo  14734  cncfss  14762  mulc1cncf  14768  cncfmptid  14776  dedekindicc  14812  ivthdec  14823  cnplimcim  14846  cnplimclemle  14847  cnplimccntop  14849  limccnp2cntop  14856  dvfgg  14867  dvcj  14888  dvrecap  14892  dvmptfsum  14904  dveflem  14905  elply2  14914  ply1termlem  14921  plymullem1  14927  eflt  14951  ptolemy  15000  cos11  15029  cxplt  15091  cxple  15092  cxplt3  15095  apcxp2  15113  rprelogbmul  15128  rprelogbdiv  15130  lgsval2lem  15167  lgsdir2lem5  15189  2sqlem6  15277  pwtrufal  15558  nninfalllem1  15568  nninfsellemqall  15575  sbthom  15586  qdencn  15587  isomninnlem  15590  trirec0  15604  apdiff  15608  iswomninnlem  15609  ismkvnnlem  15612  ltlenmkv  15630