Theorem simp2 1022

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  simpl2  1025  simpr2  1028  simp2i  1031  simp2d  1034  simp12  1052  simp22  1055  simp32  1058  syld3an3  1316  3ianorr  1343  intn3an2d  1391  stoic4b  1475  nlim0  4489  tfisi  4683  sotri2  5132  sotri3  5133  feq123  5471  sefvex  5656  fvmptt  5734  fnfvima  5884  cocan1  5923  cocan2  5924  ovexg  6047  ovmpox  6145  ovmpoga  6146  fvmpopr2d  6153  caovimo  6211  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfrcllembxssdm  6517  tfrcllembfn  6518  freccllem  6563  frecfcllem  6565  frecsuclem  6567  frecrdg  6569  domssr  6946  mapxpen  7029  dif1en  7061  diffifi  7076  unsnfidcex  7105  unfidisj  7107  undifdc  7109  resfnfinfinss  7129  funrnfi  7132  sbthlemi9  7155  elfir  7163  difinfsn  7290  ctssdc  7303  djuassen  7422  xpdjuen  7423  mulcanenq  7595  ltanqg  7610  mulcanenq0ec  7655  addnnnq0  7659  distrprg  7798  aptipr  7851  addsrpr  7955  mulsrpr  7956  mulasssrg  7968  ltpsrprg  8013  axmulass  8083  axpre-ltadd  8096  subadd2  8373  nppcan  8391  nppcan3  8393  subsub2  8397  subsub4  8402  npncan3  8407  pnpcan  8408  pnncan  8410  subcan  8424  ltadd1  8599  leadd1  8600  leadd2  8601  ltsubadd  8602  ltsubadd2  8603  lesubadd  8604  lesubadd2  8605  ltaddsub  8606  leaddsub  8608  lesub1  8626  lesub2  8627  ltsub1  8628  ltsub2  8629  gt0add  8743  apreap  8757  lemul1  8763  reapmul1lem  8764  reapmul1  8765  reapadd1  8766  remulext1  8769  remulext2  8770  apadd2  8779  mulext2  8783  mulap0r  8785  leltap  8795  ltap  8803  apsub1  8812  recexaplem2  8822  mulcanap  8835  mulcanap2  8836  divvalap  8844  divmulap  8845  divcanap1  8851  diveqap0  8852  divap0b  8853  divrecap  8858  divassap  8860  div23ap  8861  divdirap  8867  divcanap3  8868  div11ap  8870  diveqap1  8875  divmuldivap  8882  divcanap5  8884  redivclap  8901  div2negap  8905  apmul1  8958  apmul2  8959  div2subap  9007  ltdiv1  9038  ledivmul  9047  lemuldiv  9051  lt2msq1  9055  ltdiv23  9062  squeeze0  9074  ofnegsub  9132  zaddcllemneg  9508  eluzsub  9776  nn01to3  9841  rpgecl  9907  addlelt  9993  xleadd1  10100  xltadd1  10101  lbioog  10138  ubioc1  10154  ubicc2  10210  icoshftf1o  10216  fzen  10268  nelfzo  10377  ubmelfzo  10435  ssfzo12  10459  ubmelm1fzo  10461  fzosplitprm1  10470  zsupssdc  10488  rebtwn2zlemshrink  10503  qbtwnre  10506  icogelb  10515  flqwordi  10538  flqword2  10539  flltdivnn0lt  10554  modqcl  10578  mulqmod0  10582  modqmulnn  10594  modqabs2  10610  modqmuladdnn0  10620  qnegmod  10621  addmodid  10624  modqm1p1mod0  10627  modifeq2int  10638  modqdi  10644  modqeqmodmin  10646  modfzo0difsn  10647  frec2uzf1od  10658  exp3val  10793  expnegap0  10799  expgt1  10829  exprecap  10832  expmulzap  10837  leexp2a  10844  expubnd  10848  mulbinom2  10908  bernneq2  10913  expnbnd  10915  fihashss  11070  fihashssdif  11072  fimaxq  11081  ccatval2  11165  ccatass  11175  ccatw2s1leng  11205  ccat2s1fvwd  11214  swrdval  11219  swrdnd  11230  pfxfv  11255  pfxpfx  11279  ccats1pfxeq  11285  ccats1pfxeqrex  11286  s3cl  11357  s3fv0g  11362  s3fv1g  11363  s3fv2g  11364  shftuz  11368  shftfibg  11371  cjdivap  11460  resqrtcl  11580  absdivap  11621  abssubne0  11642  maxleast  11764  lemininf  11785  ltmininf  11786  xrmaxltsup  11809  xrmaxaddlem  11811  xrmaxadd  11812  xrmineqinf  11820  xrltmininf  11821  xrminltinf  11823  xrminadd  11826  climuni  11844  reccn2ap  11864  isumz  11940  geoisum1c  12071  prod1dc  12137  efltim  12249  dvdsval2  12341  dvdscmulr  12371  dvdsmulcr  12372  modmulconst  12374  dvdsadd2b  12391  dvdsexp  12412  mulmoddvds  12414  divalglemeuneg  12474  gcdaddm  12545  dvdsgcdb  12574  mulgcd  12577  gcddiv  12580  uzwodc  12598  lcmdvdsb  12646  mulgcddvds  12656  qredeq  12658  divgcdcoprm0  12663  cncongr1  12665  euclemma  12708  rpexp  12715  rpexp12i  12717  fermltl  12796  prmdiv  12797  odzcllem  12805  odzdvds  12808  odzphi  12809  vfermltl  12814  coprimeprodsq  12820  pythagtriplem6  12833  pythagtriplem7  12834  pythagtriplem12  12838  pythagtriplem13  12839  pceu  12858  pcdvdsb  12883  pcgcd1  12891  dvdsprmpweq  12898  sumhashdc  12910  ctinf  13041  fvsetsid  13106  ressressg  13148  ressabsg  13149  rngplusgg  13210  imasaddvallemg  13388  qusaddvallemg  13406  plusfvalg  13436  mgmb1mgm1  13441  issubmnd  13515  ress0g  13516  imasmnd2  13525  imasmnd  13526  gsumfzz  13568  grpasscan2  13637  grpidrcan  13638  grpidlcan  13639  grpinvadd  13651  grpsubeq0  13659  grppncan  13664  dfgrp3mlem  13671  dfgrp3me  13673  grpsubpropd2  13678  pwsinvg  13685  imasgrp2  13687  imasgrp  13688  mhmmnd  13693  mulgnn0p1  13710  mulgnnsubcl  13711  mulgnn0subcl  13712  mulgsubcl  13713  mulgneg  13717  mulgaddcom  13723  mulginvcom  13724  submmulg  13743  subgcl  13761  subgsubcl  13762  subgsub  13763  subgmulg  13765  nsgconj  13783  nsgid  13792  quseccl0g  13808  ghmmulg  13833  ghmeqker  13848  f1ghm0to0  13849  kerf1ghm  13851  ablinvadd  13887  ablsub4  13890  ablpncan2  13893  subgabl  13909  gsumfzconst  13918  rngcl  13947  imasrng  13959  srgcl  13973  ringcl  14016  crngcom  14017  ringidss  14032  ringcom  14034  imasring  14067  opprringbg  14083  unitmulcl  14117  unitmulclb  14118  dvrcl  14139  unitdvcl  14140  dvrcan1  14144  dvrcan3  14145  rhmmul  14168  subrngrng  14206  subrngmcl  14213  subrgmcl  14237  subrgdv  14242  rrgeq0  14269  domneq0  14276  islmod  14295  scafvalg  14311  lmodcom  14337  rmodislmodlem  14354  rmodislmod  14355  lssclg  14368  lssvnegcl  14380  lssintclm  14388  lspss  14403  lspun  14406  lspsnvsi  14422  rspssp  14498  rnglidlmmgm  14500  rnglidlmsgrp  14501  rnglidlrng  14502  zndvds  14653  2basgeng  14796  iuncld  14829  ntrss  14833  restco  14888  restabs  14889  cnprcl2k  14920  lmconst  14930  cnrest2  14950  cnmpt2t  15007  psmetsym  15043  psmetge0  15045  xmetge0  15079  xmetsym  15082  blvalps  15102  blval  15103  xblcntrps  15127  xblcntr  15128  xmssym  15183  blsscls2  15207  bdxmet  15215  txmetcnp  15232  dvfvalap  15395  dvid  15409  dvidre  15411  dvcnp2cntop  15413  elplyr  15454  rpcxpadd  15619  rpcxpsub  15622  rpmulcxp  15623  rpdivcxp  15625  cxpmul  15626  rpcxple2  15632  rpcxplt2  15633  rplogbval  15659  rplogbcl  15660  rplogbreexp  15667  relogbexpap  15672  logbleb  15675  logblt  15676  rplogbcxp  15677  rpcxplogb  15678  relogbcxpbap  15679  sgmppw  15706  lgsneg1  15744  lgsmod  15745  lgsne0  15757  lgssq  15759  lgsdirnn0  15766  lgsdinn0  15767  lgsquad  15799  funvtxvalg  15877  funiedgvalg  15878  lpvtx  15920  ausgrumgrien  16009  ausgrusgrien  16010  wlkl1loop  16155  clwwlknonex2  16234  findset  16476