Theorem simp2 1000

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  simpl2  1003  simpr2  1006  simp2i  1009  simp2d  1012  simp12  1030  simp22  1033  simp32  1036  syld3an3  1294  3ianorr  1320  stoic4b  1444  nlim0  4429  tfisi  4623  sotri2  5067  sotri3  5068  feq123  5399  sefvex  5579  fvmptt  5653  fnfvima  5797  cocan1  5834  cocan2  5835  ovexg  5956  ovmpox  6051  ovmpoga  6052  fvmpopr2d  6059  caovimo  6117  tfr1onlembxssdm  6401  tfr1onlembfn  6402  tfrcllembxssdm  6414  tfrcllembfn  6415  freccllem  6460  frecfcllem  6462  frecsuclem  6464  frecrdg  6466  mapxpen  6909  dif1en  6940  diffifi  6955  unsnfidcex  6981  unfidisj  6983  undifdc  6985  resfnfinfinss  7005  funrnfi  7008  sbthlemi9  7031  elfir  7039  difinfsn  7166  ctssdc  7179  djuassen  7284  xpdjuen  7285  mulcanenq  7452  ltanqg  7467  mulcanenq0ec  7512  addnnnq0  7516  distrprg  7655  aptipr  7708  addsrpr  7812  mulsrpr  7813  mulasssrg  7825  ltpsrprg  7870  axmulass  7940  axpre-ltadd  7953  subadd2  8230  nppcan  8248  nppcan3  8250  subsub2  8254  subsub4  8259  npncan3  8264  pnpcan  8265  pnncan  8267  subcan  8281  ltadd1  8456  leadd1  8457  leadd2  8458  ltsubadd  8459  ltsubadd2  8460  lesubadd  8461  lesubadd2  8462  ltaddsub  8463  leaddsub  8465  lesub1  8483  lesub2  8484  ltsub1  8485  ltsub2  8486  gt0add  8600  apreap  8614  lemul1  8620  reapmul1lem  8621  reapmul1  8622  reapadd1  8623  remulext1  8626  remulext2  8627  apadd2  8636  mulext2  8640  mulap0r  8642  leltap  8652  ltap  8660  apsub1  8669  recexaplem2  8679  mulcanap  8692  mulcanap2  8693  divvalap  8701  divmulap  8702  divcanap1  8708  diveqap0  8709  divap0b  8710  divrecap  8715  divassap  8717  div23ap  8718  divdirap  8724  divcanap3  8725  div11ap  8727  diveqap1  8732  divmuldivap  8739  divcanap5  8741  redivclap  8758  div2negap  8762  apmul1  8815  apmul2  8816  div2subap  8864  ltdiv1  8895  ledivmul  8904  lemuldiv  8908  lt2msq1  8912  ltdiv23  8919  squeeze0  8931  ofnegsub  8989  zaddcllemneg  9365  eluzsub  9631  nn01to3  9691  rpgecl  9757  addlelt  9843  xleadd1  9950  xltadd1  9951  lbioog  9988  ubioc1  10004  ubicc2  10060  icoshftf1o  10066  fzen  10118  nelfzo  10227  ubmelfzo  10276  ssfzo12  10300  ubmelm1fzo  10302  fzosplitprm1  10310  zsupssdc  10328  rebtwn2zlemshrink  10343  qbtwnre  10346  icogelb  10355  flqwordi  10378  flqword2  10379  flltdivnn0lt  10394  modqcl  10418  mulqmod0  10422  modqmulnn  10434  modqabs2  10450  modqmuladdnn0  10460  qnegmod  10461  addmodid  10464  modqm1p1mod0  10467  modifeq2int  10478  modqdi  10484  modqeqmodmin  10486  modfzo0difsn  10487  frec2uzf1od  10498  exp3val  10633  expnegap0  10639  expgt1  10669  exprecap  10672  expmulzap  10677  leexp2a  10684  expubnd  10688  mulbinom2  10748  bernneq2  10753  expnbnd  10755  fihashss  10908  fihashssdif  10910  fimaxq  10919  shftuz  10982  shftfibg  10985  cjdivap  11074  resqrtcl  11194  absdivap  11235  abssubne0  11256  maxleast  11378  lemininf  11399  ltmininf  11400  xrmaxltsup  11423  xrmaxaddlem  11425  xrmaxadd  11426  xrmineqinf  11434  xrltmininf  11435  xrminltinf  11437  xrminadd  11440  climuni  11458  reccn2ap  11478  isumz  11554  geoisum1c  11685  prod1dc  11751  efltim  11863  dvdsval2  11955  dvdscmulr  11985  dvdsmulcr  11986  modmulconst  11988  dvdsadd2b  12005  dvdsexp  12026  mulmoddvds  12028  divalglemeuneg  12088  gcdaddm  12151  dvdsgcdb  12180  mulgcd  12183  gcddiv  12186  uzwodc  12204  lcmdvdsb  12252  mulgcddvds  12262  qredeq  12264  divgcdcoprm0  12269  cncongr1  12271  euclemma  12314  rpexp  12321  rpexp12i  12323  fermltl  12402  prmdiv  12403  odzcllem  12411  odzdvds  12414  odzphi  12415  vfermltl  12420  coprimeprodsq  12426  pythagtriplem6  12439  pythagtriplem7  12440  pythagtriplem12  12444  pythagtriplem13  12445  pceu  12464  pcdvdsb  12489  pcgcd1  12497  dvdsprmpweq  12504  sumhashdc  12516  ctinf  12647  fvsetsid  12712  ressressg  12753  ressabsg  12754  rngplusgg  12814  imasaddvallemg  12958  qusaddvallemg  12976  plusfvalg  13006  mgmb1mgm1  13011  issubmnd  13083  ress0g  13084  gsumfzz  13127  grpasscan2  13196  grpidrcan  13197  grpidlcan  13198  grpinvadd  13210  grpsubeq0  13218  grppncan  13223  dfgrp3mlem  13230  dfgrp3me  13232  grpsubpropd2  13237  imasgrp2  13240  imasgrp  13241  mhmmnd  13246  mulgnn0p1  13263  mulgnnsubcl  13264  mulgnn0subcl  13265  mulgsubcl  13266  mulgneg  13270  mulgaddcom  13276  mulginvcom  13277  submmulg  13296  subgcl  13314  subgsubcl  13315  subgsub  13316  subgmulg  13318  nsgconj  13336  nsgid  13345  quseccl0g  13361  ghmmulg  13386  ghmeqker  13401  f1ghm0to0  13402  kerf1ghm  13404  ablinvadd  13440  ablsub4  13443  ablpncan2  13446  subgabl  13462  gsumfzconst  13471  rngcl  13500  imasrng  13512  srgcl  13526  ringcl  13569  crngcom  13570  ringidss  13585  ringcom  13587  imasring  13620  opprringbg  13636  unitmulcl  13669  unitmulclb  13670  dvrcl  13691  unitdvcl  13692  dvrcan1  13696  dvrcan3  13697  rhmmul  13720  subrngrng  13758  subrngmcl  13765  subrgmcl  13789  subrgdv  13794  rrgeq0  13821  domneq0  13828  islmod  13847  scafvalg  13863  lmodcom  13889  rmodislmodlem  13906  rmodislmod  13907  lssclg  13920  lssvnegcl  13932  lssintclm  13940  lspss  13955  lspun  13958  lspsnvsi  13974  rspssp  14050  rnglidlmmgm  14052  rnglidlmsgrp  14053  rnglidlrng  14054  zndvds  14205  2basgeng  14318  iuncld  14351  ntrss  14355  restco  14410  restabs  14411  cnprcl2k  14442  lmconst  14452  cnrest2  14472  cnmpt2t  14529  psmetsym  14565  psmetge0  14567  xmetge0  14601  xmetsym  14604  blvalps  14624  blval  14625  xblcntrps  14649  xblcntr  14650  xmssym  14705  blsscls2  14729  bdxmet  14737  txmetcnp  14754  dvfvalap  14917  dvid  14931  dvidre  14933  dvcnp2cntop  14935  elplyr  14976  rpcxpadd  15141  rpcxpsub  15144  rpmulcxp  15145  rpdivcxp  15147  cxpmul  15148  rpcxple2  15154  rpcxplt2  15155  rplogbval  15181  rplogbcl  15182  rplogbreexp  15189  relogbexpap  15194  logbleb  15197  logblt  15198  rplogbcxp  15199  rpcxplogb  15200  relogbcxpbap  15201  sgmppw  15228  lgsneg1  15266  lgsmod  15267  lgsne0  15279  lgssq  15281  lgsdirnn0  15288  lgsdinn0  15289  lgsquad  15321  findset  15591