Theorem simp2 1029

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

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

Proof of Theorem simp2

Step	Hyp	Ref	Expression
1		3simpa 1025	. 2 |- ( ( ph /\ ps /\ ch ) -> ( ph /\ ps ) )
2	1	simprd 114	1 |- ( ( ph /\ ps /\ ch ) -> ps )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

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

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl2  1032  simpr2  1035  simp2i  1038  simp2d  1041  simp12  1059  simp22  1062  simp32  1065  syld3an3  1323  3ianorr  1350  intn3an2d  1398  stoic4b  1482  nlim0  4541  tfisi  4736  sotri2  5188  sotri3  5189  feq123  5528  sefvex  5719  fvmptt  5800  fnfvima  5956  cocan1  5996  cocan2  5997  ovexg  6122  ovmpox  6220  ovmpoga  6221  fvmpopr2d  6228  caovimo  6286  suppval1  6483  suppimacnvfn  6490  suppfnss  6501  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfrcllembxssdm  6631  tfrcllembfn  6632  freccllem  6677  frecfcllem  6679  frecsuclem  6681  frecrdg  6683  domssr  7068  mapxpen  7152  dif1en  7187  diffifi  7202  unsnfidcex  7231  unfidisj  7233  undifdc  7235  resfnfinfinss  7257  funrnfi  7260  fissfi  7267  sbthlemi9  7287  elfir  7312  difinfsn  7446  ctssdc  7459  djuassen  7579  xpdjuen  7580  mulcanenq  7758  ltanqg  7773  mulcanenq0ec  7818  addnnnq0  7822  distrprg  7961  aptipr  8014  addsrpr  8118  mulsrpr  8119  mulasssrg  8131  ltpsrprg  8176  axmulass  8246  axpre-ltadd  8259  subadd2  8537  nppcan  8555  nppcan3  8557  subsub2  8561  subsub4  8566  npncan3  8571  pnpcan  8572  pnncan  8574  subcan  8588  ltadd1  8764  leadd1  8765  leadd2  8766  ltsubadd  8767  ltsubadd2  8768  lesubadd  8769  lesubadd2  8770  ltaddsub  8771  leaddsub  8773  lesub1  8791  lesub2  8792  ltsub1  8793  ltsub2  8794  gt0add  8909  apreap  8923  lemul1  8929  reapmul1lem  8930  reapmul1  8931  reapadd1  8932  remulext1  8935  remulext2  8936  apadd2  8945  mulext2  8949  mulap0r  8951  leltap  8961  ltap  8969  apsub1  8978  recexaplem2  8988  mulcanap  9001  mulcanap2  9002  divvalap  9012  divmulap  9013  divcanap1  9019  diveqap0  9020  divap0b  9021  divrecap  9026  divassap  9028  div23ap  9029  divdirap  9035  divcanap3  9036  div11ap  9038  diveqap1  9043  divmuldivap  9050  divcanap5  9052  redivclap  9069  div2negap  9073  apmul1  9126  apmul2  9127  div2subap  9175  ltdiv1  9206  ledivmul  9215  lemuldiv  9219  lt2msq1  9223  ltdiv23  9230  squeeze0  9242  ofsubeq0  9300  ofnegsub  9301  ind1  9309  zaddcllemneg  9694  zfidc  9734  eluzsub  9968  nn01to3  10033  rpgecl  10100  addlelt  10186  xleadd1  10294  xltadd1  10295  lbioog  10332  ubioc1  10348  ubicc2  10404  icoshftf1o  10410  fzen  10464  nelfzo  10576  ubmelfzo  10635  ssfzo12  10659  ubmelm1fzo  10661  fzosplitprm1  10670  zsupssdc  10690  rebtwn2zlemshrink  10705  qbtwnre  10708  icogelb  10717  flqwordi  10744  flqword2  10745  flltdivnn0lt  10760  modqcl  10784  mulqmod0  10788  modqmulnn  10800  modqabs2  10816  modqmuladdnn0  10826  qnegmod  10827  addmodid  10830  modqm1p1mod0  10833  modifeq2int  10844  modqdi  10850  modqeqmodmin  10852  modfzo0difsn  10853  frec2uzf1od  10864  exp3val  10999  expnegap0  11005  expgt1  11035  exprecap  11038  expmulzap  11043  leexp2a  11050  expubnd  11054  mulbinom2  11114  bernneq2  11120  expnbnd  11122  fihashss  11279  fihashssdif  11281  fimaxq  11292  ccatval2  11388  ccatass  11398  ccatw2s1leng  11428  ccat2s1fvwd  11437  swrdval  11442  swrdnd  11453  pfxfv  11478  pfxpfx  11502  ccats1pfxeq  11508  ccats1pfxeqrex  11509  s3cl  11580  s3fv0g  11585  s3fv1g  11586  s3fv2g  11587  shftuz  11604  shftfibg  11607  cjdivap  11697  resqrtcl  11817  absdivap  11858  abssubne0  11880  maxleast  12002  lemininf  12024  ltmininf  12025  xrmaxltsup  12049  xrmaxaddlem  12051  xrmaxadd  12052  xrmineqinf  12060  xrltmininf  12061  xrminltinf  12063  xrminadd  12066  climuni  12084  reccn2ap  12104  isumz  12181  geoisum1c  12312  prod1dc  12378  efltim  12490  dvdsval2  12582  dvdscmulr  12612  dvdsmulcr  12613  modmulconst  12615  dvdsadd2b  12632  dvdsexp  12653  mulmoddvds  12655  divalglemeuneg  12715  gcdaddm  12786  dvdsgcdb  12815  mulgcd  12818  gcddiv  12821  uzwodc  12839  lcmdvdsb  12887  mulgcddvds  12897  qredeq  12899  divgcdcoprm0  12904  cncongr1  12906  euclemma  12950  rpexp  12957  rpexp12i  12959  fermltl  13041  prmdiv  13042  odzcllem  13050  odzdvds  13053  odzphi  13054  vfermltl  13059  coprimeprodsq  13065  pythagtriplem6  13078  pythagtriplem7  13079  pythagtriplem12  13083  pythagtriplem13  13084  pceu  13103  pcdvdsb  13128  pcgcd1  13136  dvdsprmpweq  13143  sumhashdc  13155  ctinf  13379  fvsetsid  13444  ressressg  13488  ressabsg  13489  rngplusgg  13550  imasaddvallemg  13695  qusaddvallemg  13713  plusfvalg  13742  mgmb1mgm1  13747  issubmnd  13814  ress0g  13815  imasmnd2  13818  imasmnd  13819  grpasscan2  13928  grpidrcan  13929  grpidlcan  13930  grpinvadd  13942  grpsubeq0  13950  grppncan  13955  dfgrp3mlem  13962  dfgrp3me  13964  grpsubpropd2  13969  imasgrp2  13972  imasgrp  13973  mhmmnd  13978  mulgnn0p1  13995  mulgnnsubcl  13996  mulgnn0subcl  13997  mulgsubcl  13998  mulgneg  14002  mulgaddcom  14008  mulginvcom  14009  submmulg  14028  subgcl  14046  subgsubcl  14047  subgsub  14048  subgmulg  14050  nsgconj  14068  nsgid  14077  quseccl0g  14093  ghmmulg  14118  ghmeqker  14133  f1ghm0to0  14134  kerf1ghm  14136  ablinvadd  14204  ablsub4  14207  ablpncan2  14210  subgabl  14226  gzsumconst  14233  gsumsncmn  14246  gsumconstcmn  14266  pwsinvg  14322  rngcl  14350  imasrng  14362  srgcl  14381  ringcl  14424  crngcom  14425  ringidss  14441  ringcom  14443  imasring  14478  opprringbg  14494  unitmulcl  14529  unitmulclb  14530  dvrcl  14551  unitdvcl  14552  dvrcan1  14556  dvrcan3  14557  rhmmul  14580  subrngrng  14619  subrngmcl  14626  subrgmcl  14650  subrgdv  14655  rrgeq0  14682  domneq0  14690  islmod  14736  scafvalg  14753  lmodcom  14779  rmodislmodlem  14796  rmodislmod  14797  lssclg  14810  lssvnegcl  14822  lssintclm  14830  lspss  14845  lspun  14848  lspsnvsi  14864  rspssp  14940  rnglidlmmgm  14942  rnglidlmsgrp  14943  rnglidlrng  14944  zndvds  15093  aspss  15128  asclmul1  15138  asclmul2  15139  ascldimul  15140  asclinvg  15141  asclmulg  15153  psrbaglecl  15169  psrbagcon  15171  psrringfi  15204  2basgeng  15308  iuncld  15341  ntrss  15345  restco  15400  restabs  15401  cnprcl2k  15432  lmconst  15442  cnrest2  15462  cnmpt2t  15519  psmetsym  15555  psmetge0  15557  xmetge0  15591  xmetsym  15594  blvalps  15614  blval  15615  xblcntrps  15639  xblcntr  15640  xmssym  15695  blsscls2  15719  bdxmet  15727  txmetcnp  15744  dvfvalap  15907  dvid  15921  dvidre  15923  dvcnp2cntop  15925  elplyr  15966  logfac  16126  rpcxpadd  16138  rpcxpsub  16141  rpmulcxp  16142  rpdivcxp  16144  cxpmul  16145  rpcxple2  16153  rpcxplt2  16154  rplogbval  16181  rplogbcl  16182  rplogbreexp  16189  relogbexpap  16194  logbleb  16197  logblt  16198  rplogbcxp  16199  rpcxplogb  16200  relogbcxpbap  16201  sgmppw  16286  bcmono  16304  prmefexple  16308  lgsneg1  16349  lgsmod  16350  lgsne0  16362  lgssq  16364  lgsdirnn0  16371  lgsdinn0  16372  lgsquad  16404  funvtxvalg  16482  funiedgvalg  16483  lpvtx  16525  ausgrumgrien  16616  ausgrusgrien  16617  uhgrissubgr  16707  egrsubgr  16709  subumgredg2en  16717  subusgr  16721  wlkl1loop  16804  clwwlknonex2  16885  eulerpathprum  16926  eulerpathum  16927  findset  17176  repiecele0  17281  repiecege0  17282