Theorem simp2 1001

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 997	. 2 |- ( ( ph /\ ps /\ ch ) -> ( ph /\ ps ) )
2	1	simprd 114	1 |- ( ( ph /\ ps /\ ch ) -> ps )

Syntax hints:   -> wi 4   /\ w3a 981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  simpl2  1004  simpr2  1007  simp2i  1010  simp2d  1013  simp12  1031  simp22  1034  simp32  1037  syld3an3  1295  3ianorr  1322  intn3an2d  1369  stoic4b  1453  nlim0  4454  tfisi  4648  sotri2  5094  sotri3  5095  feq123  5432  sefvex  5615  fvmptt  5689  fnfvima  5837  cocan1  5874  cocan2  5875  ovexg  5996  ovmpox  6092  ovmpoga  6093  fvmpopr2d  6100  caovimo  6158  tfr1onlembxssdm  6447  tfr1onlembfn  6448  tfrcllembxssdm  6460  tfrcllembfn  6461  freccllem  6506  frecfcllem  6508  frecsuclem  6510  frecrdg  6512  domssr  6887  mapxpen  6965  dif1en  6997  diffifi  7012  unsnfidcex  7038  unfidisj  7040  undifdc  7042  resfnfinfinss  7062  funrnfi  7065  sbthlemi9  7088  elfir  7096  difinfsn  7223  ctssdc  7236  djuassen  7355  xpdjuen  7356  mulcanenq  7528  ltanqg  7543  mulcanenq0ec  7588  addnnnq0  7592  distrprg  7731  aptipr  7784  addsrpr  7888  mulsrpr  7889  mulasssrg  7901  ltpsrprg  7946  axmulass  8016  axpre-ltadd  8029  subadd2  8306  nppcan  8324  nppcan3  8326  subsub2  8330  subsub4  8335  npncan3  8340  pnpcan  8341  pnncan  8343  subcan  8357  ltadd1  8532  leadd1  8533  leadd2  8534  ltsubadd  8535  ltsubadd2  8536  lesubadd  8537  lesubadd2  8538  ltaddsub  8539  leaddsub  8541  lesub1  8559  lesub2  8560  ltsub1  8561  ltsub2  8562  gt0add  8676  apreap  8690  lemul1  8696  reapmul1lem  8697  reapmul1  8698  reapadd1  8699  remulext1  8702  remulext2  8703  apadd2  8712  mulext2  8716  mulap0r  8718  leltap  8728  ltap  8736  apsub1  8745  recexaplem2  8755  mulcanap  8768  mulcanap2  8769  divvalap  8777  divmulap  8778  divcanap1  8784  diveqap0  8785  divap0b  8786  divrecap  8791  divassap  8793  div23ap  8794  divdirap  8800  divcanap3  8801  div11ap  8803  diveqap1  8808  divmuldivap  8815  divcanap5  8817  redivclap  8834  div2negap  8838  apmul1  8891  apmul2  8892  div2subap  8940  ltdiv1  8971  ledivmul  8980  lemuldiv  8984  lt2msq1  8988  ltdiv23  8995  squeeze0  9007  ofnegsub  9065  zaddcllemneg  9441  eluzsub  9708  nn01to3  9768  rpgecl  9834  addlelt  9920  xleadd1  10027  xltadd1  10028  lbioog  10065  ubioc1  10081  ubicc2  10137  icoshftf1o  10143  fzen  10195  nelfzo  10304  ubmelfzo  10361  ssfzo12  10385  ubmelm1fzo  10387  fzosplitprm1  10395  zsupssdc  10413  rebtwn2zlemshrink  10428  qbtwnre  10431  icogelb  10440  flqwordi  10463  flqword2  10464  flltdivnn0lt  10479  modqcl  10503  mulqmod0  10507  modqmulnn  10519  modqabs2  10535  modqmuladdnn0  10545  qnegmod  10546  addmodid  10549  modqm1p1mod0  10552  modifeq2int  10563  modqdi  10569  modqeqmodmin  10571  modfzo0difsn  10572  frec2uzf1od  10583  exp3val  10718  expnegap0  10724  expgt1  10754  exprecap  10757  expmulzap  10762  leexp2a  10769  expubnd  10773  mulbinom2  10833  bernneq2  10838  expnbnd  10840  fihashss  10993  fihashssdif  10995  fimaxq  11004  ccatval2  11087  ccatass  11097  swrdval  11134  swrdnd  11145  pfxfv  11170  pfxpfx  11194  ccats1pfxeq  11200  ccats1pfxeqrex  11201  shftuz  11213  shftfibg  11216  cjdivap  11305  resqrtcl  11425  absdivap  11466  abssubne0  11487  maxleast  11609  lemininf  11630  ltmininf  11631  xrmaxltsup  11654  xrmaxaddlem  11656  xrmaxadd  11657  xrmineqinf  11665  xrltmininf  11666  xrminltinf  11668  xrminadd  11671  climuni  11689  reccn2ap  11709  isumz  11785  geoisum1c  11916  prod1dc  11982  efltim  12094  dvdsval2  12186  dvdscmulr  12216  dvdsmulcr  12217  modmulconst  12219  dvdsadd2b  12236  dvdsexp  12257  mulmoddvds  12259  divalglemeuneg  12319  gcdaddm  12390  dvdsgcdb  12419  mulgcd  12422  gcddiv  12425  uzwodc  12443  lcmdvdsb  12491  mulgcddvds  12501  qredeq  12503  divgcdcoprm0  12508  cncongr1  12510  euclemma  12553  rpexp  12560  rpexp12i  12562  fermltl  12641  prmdiv  12642  odzcllem  12650  odzdvds  12653  odzphi  12654  vfermltl  12659  coprimeprodsq  12665  pythagtriplem6  12678  pythagtriplem7  12679  pythagtriplem12  12683  pythagtriplem13  12684  pceu  12703  pcdvdsb  12728  pcgcd1  12736  dvdsprmpweq  12743  sumhashdc  12755  ctinf  12886  fvsetsid  12951  ressressg  12992  ressabsg  12993  rngplusgg  13054  imasaddvallemg  13232  qusaddvallemg  13250  plusfvalg  13280  mgmb1mgm1  13285  issubmnd  13359  ress0g  13360  imasmnd2  13369  imasmnd  13370  gsumfzz  13412  grpasscan2  13481  grpidrcan  13482  grpidlcan  13483  grpinvadd  13495  grpsubeq0  13503  grppncan  13508  dfgrp3mlem  13515  dfgrp3me  13517  grpsubpropd2  13522  pwsinvg  13529  imasgrp2  13531  imasgrp  13532  mhmmnd  13537  mulgnn0p1  13554  mulgnnsubcl  13555  mulgnn0subcl  13556  mulgsubcl  13557  mulgneg  13561  mulgaddcom  13567  mulginvcom  13568  submmulg  13587  subgcl  13605  subgsubcl  13606  subgsub  13607  subgmulg  13609  nsgconj  13627  nsgid  13636  quseccl0g  13652  ghmmulg  13677  ghmeqker  13692  f1ghm0to0  13693  kerf1ghm  13695  ablinvadd  13731  ablsub4  13734  ablpncan2  13737  subgabl  13753  gsumfzconst  13762  rngcl  13791  imasrng  13803  srgcl  13817  ringcl  13860  crngcom  13861  ringidss  13876  ringcom  13878  imasring  13911  opprringbg  13927  unitmulcl  13960  unitmulclb  13961  dvrcl  13982  unitdvcl  13983  dvrcan1  13987  dvrcan3  13988  rhmmul  14011  subrngrng  14049  subrngmcl  14056  subrgmcl  14080  subrgdv  14085  rrgeq0  14112  domneq0  14119  islmod  14138  scafvalg  14154  lmodcom  14180  rmodislmodlem  14197  rmodislmod  14198  lssclg  14211  lssvnegcl  14223  lssintclm  14231  lspss  14246  lspun  14249  lspsnvsi  14265  rspssp  14341  rnglidlmmgm  14343  rnglidlmsgrp  14344  rnglidlrng  14345  zndvds  14496  2basgeng  14639  iuncld  14672  ntrss  14676  restco  14731  restabs  14732  cnprcl2k  14763  lmconst  14773  cnrest2  14793  cnmpt2t  14850  psmetsym  14886  psmetge0  14888  xmetge0  14922  xmetsym  14925  blvalps  14945  blval  14946  xblcntrps  14970  xblcntr  14971  xmssym  15026  blsscls2  15050  bdxmet  15058  txmetcnp  15075  dvfvalap  15238  dvid  15252  dvidre  15254  dvcnp2cntop  15256  elplyr  15297  rpcxpadd  15462  rpcxpsub  15465  rpmulcxp  15466  rpdivcxp  15468  cxpmul  15469  rpcxple2  15475  rpcxplt2  15476  rplogbval  15502  rplogbcl  15503  rplogbreexp  15510  relogbexpap  15515  logbleb  15518  logblt  15519  rplogbcxp  15520  rpcxplogb  15521  relogbcxpbap  15522  sgmppw  15549  lgsneg1  15587  lgsmod  15588  lgsne0  15600  lgssq  15602  lgsdirnn0  15609  lgsdinn0  15610  lgsquad  15642  funvtxvalg  15720  funiedgvalg  15721  lpvtx  15760  findset  16050