Theorem simp2 1025

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  simpl2  1028  simpr2  1031  simp2i  1034  simp2d  1037  simp12  1055  simp22  1058  simp32  1061  syld3an3  1319  3ianorr  1346  intn3an2d  1394  stoic4b  1478  nlim0  4497  tfisi  4691  sotri2  5141  sotri3  5142  feq123  5481  sefvex  5669  fvmptt  5747  fnfvima  5899  cocan1  5938  cocan2  5939  ovexg  6062  ovmpox  6160  ovmpoga  6161  fvmpopr2d  6168  caovimo  6226  suppval1  6417  suppimacnvfn  6424  suppfnss  6435  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfrcllembxssdm  6565  tfrcllembfn  6566  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecrdg  6617  domssr  6994  mapxpen  7077  dif1en  7111  diffifi  7126  unsnfidcex  7155  unfidisj  7157  undifdc  7159  resfnfinfinss  7181  funrnfi  7184  sbthlemi9  7207  elfir  7215  difinfsn  7342  ctssdc  7355  djuassen  7475  xpdjuen  7476  mulcanenq  7648  ltanqg  7663  mulcanenq0ec  7708  addnnnq0  7712  distrprg  7851  aptipr  7904  addsrpr  8008  mulsrpr  8009  mulasssrg  8021  ltpsrprg  8066  axmulass  8136  axpre-ltadd  8149  subadd2  8425  nppcan  8443  nppcan3  8445  subsub2  8449  subsub4  8454  npncan3  8459  pnpcan  8460  pnncan  8462  subcan  8476  ltadd1  8651  leadd1  8652  leadd2  8653  ltsubadd  8654  ltsubadd2  8655  lesubadd  8656  lesubadd2  8657  ltaddsub  8658  leaddsub  8660  lesub1  8678  lesub2  8679  ltsub1  8680  ltsub2  8681  gt0add  8795  apreap  8809  lemul1  8815  reapmul1lem  8816  reapmul1  8817  reapadd1  8818  remulext1  8821  remulext2  8822  apadd2  8831  mulext2  8835  mulap0r  8837  leltap  8847  ltap  8855  apsub1  8864  recexaplem2  8874  mulcanap  8887  mulcanap2  8888  divvalap  8896  divmulap  8897  divcanap1  8903  diveqap0  8904  divap0b  8905  divrecap  8910  divassap  8912  div23ap  8913  divdirap  8919  divcanap3  8920  div11ap  8922  diveqap1  8927  divmuldivap  8934  divcanap5  8936  redivclap  8953  div2negap  8957  apmul1  9010  apmul2  9011  div2subap  9059  ltdiv1  9090  ledivmul  9099  lemuldiv  9103  lt2msq1  9107  ltdiv23  9114  squeeze0  9126  ofnegsub  9184  zaddcllemneg  9562  eluzsub  9830  nn01to3  9895  rpgecl  9961  addlelt  10047  xleadd1  10154  xltadd1  10155  lbioog  10192  ubioc1  10208  ubicc2  10264  icoshftf1o  10270  fzen  10323  nelfzo  10432  ubmelfzo  10491  ssfzo12  10515  ubmelm1fzo  10517  fzosplitprm1  10526  zsupssdc  10544  rebtwn2zlemshrink  10559  qbtwnre  10562  icogelb  10571  flqwordi  10594  flqword2  10595  flltdivnn0lt  10610  modqcl  10634  mulqmod0  10638  modqmulnn  10650  modqabs2  10666  modqmuladdnn0  10676  qnegmod  10677  addmodid  10680  modqm1p1mod0  10683  modifeq2int  10694  modqdi  10700  modqeqmodmin  10702  modfzo0difsn  10703  frec2uzf1od  10714  exp3val  10849  expnegap0  10855  expgt1  10885  exprecap  10888  expmulzap  10893  leexp2a  10900  expubnd  10904  mulbinom2  10964  bernneq2  10969  expnbnd  10971  fihashss  11126  fihashssdif  11128  fimaxq  11137  ccatval2  11224  ccatass  11234  ccatw2s1leng  11264  ccat2s1fvwd  11273  swrdval  11278  swrdnd  11289  pfxfv  11314  pfxpfx  11338  ccats1pfxeq  11344  ccats1pfxeqrex  11345  s3cl  11416  s3fv0g  11421  s3fv1g  11422  s3fv2g  11423  shftuz  11440  shftfibg  11443  cjdivap  11532  resqrtcl  11652  absdivap  11693  abssubne0  11714  maxleast  11836  lemininf  11857  ltmininf  11858  xrmaxltsup  11881  xrmaxaddlem  11883  xrmaxadd  11884  xrmineqinf  11892  xrltmininf  11893  xrminltinf  11895  xrminadd  11898  climuni  11916  reccn2ap  11936  isumz  12013  geoisum1c  12144  prod1dc  12210  efltim  12322  dvdsval2  12414  dvdscmulr  12444  dvdsmulcr  12445  modmulconst  12447  dvdsadd2b  12464  dvdsexp  12485  mulmoddvds  12487  divalglemeuneg  12547  gcdaddm  12618  dvdsgcdb  12647  mulgcd  12650  gcddiv  12653  uzwodc  12671  lcmdvdsb  12719  mulgcddvds  12729  qredeq  12731  divgcdcoprm0  12736  cncongr1  12738  euclemma  12781  rpexp  12788  rpexp12i  12790  fermltl  12869  prmdiv  12870  odzcllem  12878  odzdvds  12881  odzphi  12882  vfermltl  12887  coprimeprodsq  12893  pythagtriplem6  12906  pythagtriplem7  12907  pythagtriplem12  12911  pythagtriplem13  12912  pceu  12931  pcdvdsb  12956  pcgcd1  12964  dvdsprmpweq  12971  sumhashdc  12983  ctinf  13114  fvsetsid  13179  ressressg  13221  ressabsg  13222  rngplusgg  13283  imasaddvallemg  13461  qusaddvallemg  13479  plusfvalg  13509  mgmb1mgm1  13514  issubmnd  13588  ress0g  13589  imasmnd2  13598  imasmnd  13599  gsumfzz  13641  grpasscan2  13710  grpidrcan  13711  grpidlcan  13712  grpinvadd  13724  grpsubeq0  13732  grppncan  13737  dfgrp3mlem  13744  dfgrp3me  13746  grpsubpropd2  13751  pwsinvg  13758  imasgrp2  13760  imasgrp  13761  mhmmnd  13766  mulgnn0p1  13783  mulgnnsubcl  13784  mulgnn0subcl  13785  mulgsubcl  13786  mulgneg  13790  mulgaddcom  13796  mulginvcom  13797  submmulg  13816  subgcl  13834  subgsubcl  13835  subgsub  13836  subgmulg  13838  nsgconj  13856  nsgid  13865  quseccl0g  13881  ghmmulg  13906  ghmeqker  13921  f1ghm0to0  13922  kerf1ghm  13924  ablinvadd  13960  ablsub4  13963  ablpncan2  13966  subgabl  13982  gsumfzconst  13991  rngcl  14021  imasrng  14033  srgcl  14047  ringcl  14090  crngcom  14091  ringidss  14106  ringcom  14108  imasring  14141  opprringbg  14157  unitmulcl  14191  unitmulclb  14192  dvrcl  14213  unitdvcl  14214  dvrcan1  14218  dvrcan3  14219  rhmmul  14242  subrngrng  14280  subrngmcl  14287  subrgmcl  14311  subrgdv  14316  rrgeq0  14343  domneq0  14351  islmod  14370  scafvalg  14386  lmodcom  14412  rmodislmodlem  14429  rmodislmod  14430  lssclg  14443  lssvnegcl  14455  lssintclm  14463  lspss  14478  lspun  14481  lspsnvsi  14497  rspssp  14573  rnglidlmmgm  14575  rnglidlmsgrp  14576  rnglidlrng  14577  zndvds  14728  psrbaglecl  14754  psrbagcon  14755  2basgeng  14876  iuncld  14909  ntrss  14913  restco  14968  restabs  14969  cnprcl2k  15000  lmconst  15010  cnrest2  15030  cnmpt2t  15087  psmetsym  15123  psmetge0  15125  xmetge0  15159  xmetsym  15162  blvalps  15182  blval  15183  xblcntrps  15207  xblcntr  15208  xmssym  15263  blsscls2  15287  bdxmet  15295  txmetcnp  15312  dvfvalap  15475  dvid  15489  dvidre  15491  dvcnp2cntop  15493  elplyr  15534  rpcxpadd  15699  rpcxpsub  15702  rpmulcxp  15703  rpdivcxp  15705  cxpmul  15706  rpcxple2  15712  rpcxplt2  15713  rplogbval  15739  rplogbcl  15740  rplogbreexp  15747  relogbexpap  15752  logbleb  15755  logblt  15756  rplogbcxp  15757  rpcxplogb  15758  relogbcxpbap  15759  sgmppw  15789  lgsneg1  15827  lgsmod  15828  lgsne0  15840  lgssq  15842  lgsdirnn0  15849  lgsdinn0  15850  lgsquad  15882  funvtxvalg  15960  funiedgvalg  15961  lpvtx  16003  ausgrumgrien  16094  ausgrusgrien  16095  uhgrissubgr  16185  egrsubgr  16187  subumgredg2en  16195  subusgr  16199  wlkl1loop  16282  clwwlknonex2  16363  eulerpathprum  16404  eulerpathum  16405  findset  16644  repiecele0  16741  repiecege0  16742  gfsumsn  16797