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  4441  tfisi  4635  sotri2  5080  sotri3  5081  feq123  5417  sefvex  5597  fvmptt  5671  fnfvima  5819  cocan1  5856  cocan2  5857  ovexg  5978  ovmpox  6074  ovmpoga  6075  fvmpopr2d  6082  caovimo  6140  tfr1onlembxssdm  6429  tfr1onlembfn  6430  tfrcllembxssdm  6442  tfrcllembfn  6443  freccllem  6488  frecfcllem  6490  frecsuclem  6492  frecrdg  6494  domssr  6869  mapxpen  6945  dif1en  6976  diffifi  6991  unsnfidcex  7017  unfidisj  7019  undifdc  7021  resfnfinfinss  7041  funrnfi  7044  sbthlemi9  7067  elfir  7075  difinfsn  7202  ctssdc  7215  djuassen  7329  xpdjuen  7330  mulcanenq  7498  ltanqg  7513  mulcanenq0ec  7558  addnnnq0  7562  distrprg  7701  aptipr  7754  addsrpr  7858  mulsrpr  7859  mulasssrg  7871  ltpsrprg  7916  axmulass  7986  axpre-ltadd  7999  subadd2  8276  nppcan  8294  nppcan3  8296  subsub2  8300  subsub4  8305  npncan3  8310  pnpcan  8311  pnncan  8313  subcan  8327  ltadd1  8502  leadd1  8503  leadd2  8504  ltsubadd  8505  ltsubadd2  8506  lesubadd  8507  lesubadd2  8508  ltaddsub  8509  leaddsub  8511  lesub1  8529  lesub2  8530  ltsub1  8531  ltsub2  8532  gt0add  8646  apreap  8660  lemul1  8666  reapmul1lem  8667  reapmul1  8668  reapadd1  8669  remulext1  8672  remulext2  8673  apadd2  8682  mulext2  8686  mulap0r  8688  leltap  8698  ltap  8706  apsub1  8715  recexaplem2  8725  mulcanap  8738  mulcanap2  8739  divvalap  8747  divmulap  8748  divcanap1  8754  diveqap0  8755  divap0b  8756  divrecap  8761  divassap  8763  div23ap  8764  divdirap  8770  divcanap3  8771  div11ap  8773  diveqap1  8778  divmuldivap  8785  divcanap5  8787  redivclap  8804  div2negap  8808  apmul1  8861  apmul2  8862  div2subap  8910  ltdiv1  8941  ledivmul  8950  lemuldiv  8954  lt2msq1  8958  ltdiv23  8965  squeeze0  8977  ofnegsub  9035  zaddcllemneg  9411  eluzsub  9678  nn01to3  9738  rpgecl  9804  addlelt  9890  xleadd1  9997  xltadd1  9998  lbioog  10035  ubioc1  10051  ubicc2  10107  icoshftf1o  10113  fzen  10165  nelfzo  10274  ubmelfzo  10329  ssfzo12  10353  ubmelm1fzo  10355  fzosplitprm1  10363  zsupssdc  10381  rebtwn2zlemshrink  10396  qbtwnre  10399  icogelb  10408  flqwordi  10431  flqword2  10432  flltdivnn0lt  10447  modqcl  10471  mulqmod0  10475  modqmulnn  10487  modqabs2  10503  modqmuladdnn0  10513  qnegmod  10514  addmodid  10517  modqm1p1mod0  10520  modifeq2int  10531  modqdi  10537  modqeqmodmin  10539  modfzo0difsn  10540  frec2uzf1od  10551  exp3val  10686  expnegap0  10692  expgt1  10722  exprecap  10725  expmulzap  10730  leexp2a  10737  expubnd  10741  mulbinom2  10801  bernneq2  10806  expnbnd  10808  fihashss  10961  fihashssdif  10963  fimaxq  10972  ccatval2  11054  ccatass  11064  swrdval  11101  swrdnd  11112  shftuz  11128  shftfibg  11131  cjdivap  11220  resqrtcl  11340  absdivap  11381  abssubne0  11402  maxleast  11524  lemininf  11545  ltmininf  11546  xrmaxltsup  11569  xrmaxaddlem  11571  xrmaxadd  11572  xrmineqinf  11580  xrltmininf  11581  xrminltinf  11583  xrminadd  11586  climuni  11604  reccn2ap  11624  isumz  11700  geoisum1c  11831  prod1dc  11897  efltim  12009  dvdsval2  12101  dvdscmulr  12131  dvdsmulcr  12132  modmulconst  12134  dvdsadd2b  12151  dvdsexp  12172  mulmoddvds  12174  divalglemeuneg  12234  gcdaddm  12305  dvdsgcdb  12334  mulgcd  12337  gcddiv  12340  uzwodc  12358  lcmdvdsb  12406  mulgcddvds  12416  qredeq  12418  divgcdcoprm0  12423  cncongr1  12425  euclemma  12468  rpexp  12475  rpexp12i  12477  fermltl  12556  prmdiv  12557  odzcllem  12565  odzdvds  12568  odzphi  12569  vfermltl  12574  coprimeprodsq  12580  pythagtriplem6  12593  pythagtriplem7  12594  pythagtriplem12  12598  pythagtriplem13  12599  pceu  12618  pcdvdsb  12643  pcgcd1  12651  dvdsprmpweq  12658  sumhashdc  12670  ctinf  12801  fvsetsid  12866  ressressg  12907  ressabsg  12908  rngplusgg  12969  imasaddvallemg  13147  qusaddvallemg  13165  plusfvalg  13195  mgmb1mgm1  13200  issubmnd  13274  ress0g  13275  imasmnd2  13284  imasmnd  13285  gsumfzz  13327  grpasscan2  13396  grpidrcan  13397  grpidlcan  13398  grpinvadd  13410  grpsubeq0  13418  grppncan  13423  dfgrp3mlem  13430  dfgrp3me  13432  grpsubpropd2  13437  pwsinvg  13444  imasgrp2  13446  imasgrp  13447  mhmmnd  13452  mulgnn0p1  13469  mulgnnsubcl  13470  mulgnn0subcl  13471  mulgsubcl  13472  mulgneg  13476  mulgaddcom  13482  mulginvcom  13483  submmulg  13502  subgcl  13520  subgsubcl  13521  subgsub  13522  subgmulg  13524  nsgconj  13542  nsgid  13551  quseccl0g  13567  ghmmulg  13592  ghmeqker  13607  f1ghm0to0  13608  kerf1ghm  13610  ablinvadd  13646  ablsub4  13649  ablpncan2  13652  subgabl  13668  gsumfzconst  13677  rngcl  13706  imasrng  13718  srgcl  13732  ringcl  13775  crngcom  13776  ringidss  13791  ringcom  13793  imasring  13826  opprringbg  13842  unitmulcl  13875  unitmulclb  13876  dvrcl  13897  unitdvcl  13898  dvrcan1  13902  dvrcan3  13903  rhmmul  13926  subrngrng  13964  subrngmcl  13971  subrgmcl  13995  subrgdv  14000  rrgeq0  14027  domneq0  14034  islmod  14053  scafvalg  14069  lmodcom  14095  rmodislmodlem  14112  rmodislmod  14113  lssclg  14126  lssvnegcl  14138  lssintclm  14146  lspss  14161  lspun  14164  lspsnvsi  14180  rspssp  14256  rnglidlmmgm  14258  rnglidlmsgrp  14259  rnglidlrng  14260  zndvds  14411  2basgeng  14554  iuncld  14587  ntrss  14591  restco  14646  restabs  14647  cnprcl2k  14678  lmconst  14688  cnrest2  14708  cnmpt2t  14765  psmetsym  14801  psmetge0  14803  xmetge0  14837  xmetsym  14840  blvalps  14860  blval  14861  xblcntrps  14885  xblcntr  14886  xmssym  14941  blsscls2  14965  bdxmet  14973  txmetcnp  14990  dvfvalap  15153  dvid  15167  dvidre  15169  dvcnp2cntop  15171  elplyr  15212  rpcxpadd  15377  rpcxpsub  15380  rpmulcxp  15381  rpdivcxp  15383  cxpmul  15384  rpcxple2  15390  rpcxplt2  15391  rplogbval  15417  rplogbcl  15418  rplogbreexp  15425  relogbexpap  15430  logbleb  15433  logblt  15434  rplogbcxp  15435  rpcxplogb  15436  relogbcxpbap  15437  sgmppw  15464  lgsneg1  15502  lgsmod  15503  lgsne0  15515  lgssq  15517  lgsdirnn0  15524  lgsdinn0  15525  lgsquad  15557  funvtxvalg  15633  funiedgvalg  15634  findset  15881