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  4539  tfisi  4734  sotri2  5185  sotri3  5186  feq123  5525  sefvex  5716  fvmptt  5797  fnfvima  5953  cocan1  5993  cocan2  5994  ovexg  6119  ovmpox  6217  ovmpoga  6218  fvmpopr2d  6225  caovimo  6283  suppval1  6479  suppimacnvfn  6486  suppfnss  6497  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfrcllembxssdm  6627  tfrcllembfn  6628  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecrdg  6679  domssr  7064  mapxpen  7148  dif1en  7183  diffifi  7198  unsnfidcex  7227  unfidisj  7229  undifdc  7231  resfnfinfinss  7253  funrnfi  7256  fissfi  7263  sbthlemi9  7282  elfir  7307  difinfsn  7441  ctssdc  7454  djuassen  7574  xpdjuen  7575  mulcanenq  7753  ltanqg  7768  mulcanenq0ec  7813  addnnnq0  7817  distrprg  7956  aptipr  8009  addsrpr  8113  mulsrpr  8114  mulasssrg  8126  ltpsrprg  8171  axmulass  8241  axpre-ltadd  8254  subadd2  8532  nppcan  8550  nppcan3  8552  subsub2  8556  subsub4  8561  npncan3  8566  pnpcan  8567  pnncan  8569  subcan  8583  ltadd1  8759  leadd1  8760  leadd2  8761  ltsubadd  8762  ltsubadd2  8763  lesubadd  8764  lesubadd2  8765  ltaddsub  8766  leaddsub  8768  lesub1  8786  lesub2  8787  ltsub1  8788  ltsub2  8789  gt0add  8904  apreap  8918  lemul1  8924  reapmul1lem  8925  reapmul1  8926  reapadd1  8927  remulext1  8930  remulext2  8931  apadd2  8940  mulext2  8944  mulap0r  8946  leltap  8956  ltap  8964  apsub1  8973  recexaplem2  8983  mulcanap  8996  mulcanap2  8997  divvalap  9007  divmulap  9008  divcanap1  9014  diveqap0  9015  divap0b  9016  divrecap  9021  divassap  9023  div23ap  9024  divdirap  9030  divcanap3  9031  div11ap  9033  diveqap1  9038  divmuldivap  9045  divcanap5  9047  redivclap  9064  div2negap  9068  apmul1  9121  apmul2  9122  div2subap  9170  ltdiv1  9201  ledivmul  9210  lemuldiv  9214  lt2msq1  9218  ltdiv23  9225  squeeze0  9237  ofnegsub  9295  ind1  9303  zaddcllemneg  9688  zfidc  9728  eluzsub  9962  nn01to3  10027  rpgecl  10094  addlelt  10180  xleadd1  10288  xltadd1  10289  lbioog  10326  ubioc1  10342  ubicc2  10398  icoshftf1o  10404  fzen  10458  nelfzo  10570  ubmelfzo  10629  ssfzo12  10653  ubmelm1fzo  10655  fzosplitprm1  10664  zsupssdc  10684  rebtwn2zlemshrink  10699  qbtwnre  10702  icogelb  10711  flqwordi  10738  flqword2  10739  flltdivnn0lt  10754  modqcl  10778  mulqmod0  10782  modqmulnn  10794  modqabs2  10810  modqmuladdnn0  10820  qnegmod  10821  addmodid  10824  modqm1p1mod0  10827  modifeq2int  10838  modqdi  10844  modqeqmodmin  10846  modfzo0difsn  10847  frec2uzf1od  10858  exp3val  10993  expnegap0  10999  expgt1  11029  exprecap  11032  expmulzap  11037  leexp2a  11044  expubnd  11048  mulbinom2  11108  bernneq2  11114  expnbnd  11116  fihashss  11273  fihashssdif  11275  fimaxq  11286  ccatval2  11382  ccatass  11392  ccatw2s1leng  11422  ccat2s1fvwd  11431  swrdval  11436  swrdnd  11447  pfxfv  11472  pfxpfx  11496  ccats1pfxeq  11502  ccats1pfxeqrex  11503  s3cl  11574  s3fv0g  11579  s3fv1g  11580  s3fv2g  11581  shftuz  11598  shftfibg  11601  cjdivap  11691  resqrtcl  11811  absdivap  11852  abssubne0  11874  maxleast  11996  lemininf  12018  ltmininf  12019  xrmaxltsup  12043  xrmaxaddlem  12045  xrmaxadd  12046  xrmineqinf  12054  xrltmininf  12055  xrminltinf  12057  xrminadd  12060  climuni  12078  reccn2ap  12098  isumz  12175  geoisum1c  12306  prod1dc  12372  efltim  12484  dvdsval2  12576  dvdscmulr  12606  dvdsmulcr  12607  modmulconst  12609  dvdsadd2b  12626  dvdsexp  12647  mulmoddvds  12649  divalglemeuneg  12709  gcdaddm  12780  dvdsgcdb  12809  mulgcd  12812  gcddiv  12815  uzwodc  12833  lcmdvdsb  12881  mulgcddvds  12891  qredeq  12893  divgcdcoprm0  12898  cncongr1  12900  euclemma  12944  rpexp  12951  rpexp12i  12953  fermltl  13035  prmdiv  13036  odzcllem  13044  odzdvds  13047  odzphi  13048  vfermltl  13053  coprimeprodsq  13059  pythagtriplem6  13072  pythagtriplem7  13073  pythagtriplem12  13077  pythagtriplem13  13078  pceu  13097  pcdvdsb  13122  pcgcd1  13130  dvdsprmpweq  13137  sumhashdc  13149  ctinf  13373  fvsetsid  13438  ressressg  13482  ressabsg  13483  rngplusgg  13544  imasaddvallemg  13689  qusaddvallemg  13707  plusfvalg  13736  mgmb1mgm1  13741  issubmnd  13808  ress0g  13809  imasmnd2  13812  imasmnd  13813  grpasscan2  13922  grpidrcan  13923  grpidlcan  13924  grpinvadd  13936  grpsubeq0  13944  grppncan  13949  dfgrp3mlem  13956  dfgrp3me  13958  grpsubpropd2  13963  imasgrp2  13966  imasgrp  13967  mhmmnd  13972  mulgnn0p1  13989  mulgnnsubcl  13990  mulgnn0subcl  13991  mulgsubcl  13992  mulgneg  13996  mulgaddcom  14002  mulginvcom  14003  submmulg  14022  subgcl  14040  subgsubcl  14041  subgsub  14042  subgmulg  14044  nsgconj  14062  nsgid  14071  quseccl0g  14087  ghmmulg  14112  ghmeqker  14127  f1ghm0to0  14128  kerf1ghm  14130  ablinvadd  14198  ablsub4  14201  ablpncan2  14204  subgabl  14220  gzsumconst  14227  gsumsncmn  14240  gsumconstcmn  14250  pwsinvg  14299  rngcl  14327  imasrng  14339  srgcl  14358  ringcl  14401  crngcom  14402  ringidss  14418  ringcom  14420  imasring  14453  opprringbg  14469  unitmulcl  14504  unitmulclb  14505  dvrcl  14526  unitdvcl  14527  dvrcan1  14531  dvrcan3  14532  rhmmul  14555  subrngrng  14594  subrngmcl  14601  subrgmcl  14625  subrgdv  14630  rrgeq0  14657  domneq0  14665  islmod  14711  scafvalg  14728  lmodcom  14754  rmodislmodlem  14771  rmodislmod  14772  lssclg  14785  lssvnegcl  14797  lssintclm  14805  lspss  14820  lspun  14823  lspsnvsi  14839  rspssp  14915  rnglidlmmgm  14917  rnglidlmsgrp  14918  rnglidlrng  14919  zndvds  15068  aspss  15103  asclmul1  15113  asclmul2  15114  ascldimul  15115  asclinvg  15116  asclmulg  15128  psrbaglecl  15144  psrbagcon  15146  2basgeng  15274  iuncld  15307  ntrss  15311  restco  15366  restabs  15367  cnprcl2k  15398  lmconst  15408  cnrest2  15428  cnmpt2t  15485  psmetsym  15521  psmetge0  15523  xmetge0  15557  xmetsym  15560  blvalps  15580  blval  15581  xblcntrps  15605  xblcntr  15606  xmssym  15661  blsscls2  15685  bdxmet  15693  txmetcnp  15710  dvfvalap  15873  dvid  15887  dvidre  15889  dvcnp2cntop  15891  elplyr  15932  logfac  16090  rpcxpadd  16102  rpcxpsub  16105  rpmulcxp  16106  rpdivcxp  16108  cxpmul  16109  rpcxple2  16115  rpcxplt2  16116  rplogbval  16142  rplogbcl  16143  rplogbreexp  16150  relogbexpap  16155  logbleb  16158  logblt  16159  rplogbcxp  16160  rpcxplogb  16161  relogbcxpbap  16162  sgmppw  16247  bcmono  16265  prmefexple  16269  lgsneg1  16310  lgsmod  16311  lgsne0  16323  lgssq  16325  lgsdirnn0  16332  lgsdinn0  16333  lgsquad  16365  funvtxvalg  16443  funiedgvalg  16444  lpvtx  16486  ausgrumgrien  16577  ausgrusgrien  16578  uhgrissubgr  16668  egrsubgr  16670  subumgredg2en  16678  subusgr  16682  wlkl1loop  16765  clwwlknonex2  16846  eulerpathprum  16887  eulerpathum  16888  findset  17137  repiecele0  17241  repiecege0  17242