Theorem simp2 1024

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

Syntax hints:   -> wi 4   /\ w3a 1004

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 1006

This theorem is referenced by:  simpl2  1027  simpr2  1030  simp2i  1033  simp2d  1036  simp12  1054  simp22  1057  simp32  1060  syld3an3  1318  3ianorr  1345  intn3an2d  1393  stoic4b  1477  nlim0  4491  tfisi  4685  sotri2  5134  sotri3  5135  feq123  5474  sefvex  5660  fvmptt  5738  fnfvima  5889  cocan1  5928  cocan2  5929  ovexg  6052  ovmpox  6150  ovmpoga  6151  fvmpopr2d  6158  caovimo  6216  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfrcllembxssdm  6522  tfrcllembfn  6523  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecrdg  6574  domssr  6951  mapxpen  7034  dif1en  7068  diffifi  7083  unsnfidcex  7112  unfidisj  7114  undifdc  7116  resfnfinfinss  7138  funrnfi  7141  sbthlemi9  7164  elfir  7172  difinfsn  7299  ctssdc  7312  djuassen  7432  xpdjuen  7433  mulcanenq  7605  ltanqg  7620  mulcanenq0ec  7665  addnnnq0  7669  distrprg  7808  aptipr  7861  addsrpr  7965  mulsrpr  7966  mulasssrg  7978  ltpsrprg  8023  axmulass  8093  axpre-ltadd  8106  subadd2  8383  nppcan  8401  nppcan3  8403  subsub2  8407  subsub4  8412  npncan3  8417  pnpcan  8418  pnncan  8420  subcan  8434  ltadd1  8609  leadd1  8610  leadd2  8611  ltsubadd  8612  ltsubadd2  8613  lesubadd  8614  lesubadd2  8615  ltaddsub  8616  leaddsub  8618  lesub1  8636  lesub2  8637  ltsub1  8638  ltsub2  8639  gt0add  8753  apreap  8767  lemul1  8773  reapmul1lem  8774  reapmul1  8775  reapadd1  8776  remulext1  8779  remulext2  8780  apadd2  8789  mulext2  8793  mulap0r  8795  leltap  8805  ltap  8813  apsub1  8822  recexaplem2  8832  mulcanap  8845  mulcanap2  8846  divvalap  8854  divmulap  8855  divcanap1  8861  diveqap0  8862  divap0b  8863  divrecap  8868  divassap  8870  div23ap  8871  divdirap  8877  divcanap3  8878  div11ap  8880  diveqap1  8885  divmuldivap  8892  divcanap5  8894  redivclap  8911  div2negap  8915  apmul1  8968  apmul2  8969  div2subap  9017  ltdiv1  9048  ledivmul  9057  lemuldiv  9061  lt2msq1  9065  ltdiv23  9072  squeeze0  9084  ofnegsub  9142  zaddcllemneg  9518  eluzsub  9786  nn01to3  9851  rpgecl  9917  addlelt  10003  xleadd1  10110  xltadd1  10111  lbioog  10148  ubioc1  10164  ubicc2  10220  icoshftf1o  10226  fzen  10278  nelfzo  10387  ubmelfzo  10446  ssfzo12  10470  ubmelm1fzo  10472  fzosplitprm1  10481  zsupssdc  10499  rebtwn2zlemshrink  10514  qbtwnre  10517  icogelb  10526  flqwordi  10549  flqword2  10550  flltdivnn0lt  10565  modqcl  10589  mulqmod0  10593  modqmulnn  10605  modqabs2  10621  modqmuladdnn0  10631  qnegmod  10632  addmodid  10635  modqm1p1mod0  10638  modifeq2int  10649  modqdi  10655  modqeqmodmin  10657  modfzo0difsn  10658  frec2uzf1od  10669  exp3val  10804  expnegap0  10810  expgt1  10840  exprecap  10843  expmulzap  10848  leexp2a  10855  expubnd  10859  mulbinom2  10919  bernneq2  10924  expnbnd  10926  fihashss  11081  fihashssdif  11083  fimaxq  11092  ccatval2  11179  ccatass  11189  ccatw2s1leng  11219  ccat2s1fvwd  11228  swrdval  11233  swrdnd  11244  pfxfv  11269  pfxpfx  11293  ccats1pfxeq  11299  ccats1pfxeqrex  11300  s3cl  11371  s3fv0g  11376  s3fv1g  11377  s3fv2g  11378  shftuz  11382  shftfibg  11385  cjdivap  11474  resqrtcl  11594  absdivap  11635  abssubne0  11656  maxleast  11778  lemininf  11799  ltmininf  11800  xrmaxltsup  11823  xrmaxaddlem  11825  xrmaxadd  11826  xrmineqinf  11834  xrltmininf  11835  xrminltinf  11837  xrminadd  11840  climuni  11858  reccn2ap  11878  isumz  11955  geoisum1c  12086  prod1dc  12152  efltim  12264  dvdsval2  12356  dvdscmulr  12386  dvdsmulcr  12387  modmulconst  12389  dvdsadd2b  12406  dvdsexp  12427  mulmoddvds  12429  divalglemeuneg  12489  gcdaddm  12560  dvdsgcdb  12589  mulgcd  12592  gcddiv  12595  uzwodc  12613  lcmdvdsb  12661  mulgcddvds  12671  qredeq  12673  divgcdcoprm0  12678  cncongr1  12680  euclemma  12723  rpexp  12730  rpexp12i  12732  fermltl  12811  prmdiv  12812  odzcllem  12820  odzdvds  12823  odzphi  12824  vfermltl  12829  coprimeprodsq  12835  pythagtriplem6  12848  pythagtriplem7  12849  pythagtriplem12  12853  pythagtriplem13  12854  pceu  12873  pcdvdsb  12898  pcgcd1  12906  dvdsprmpweq  12913  sumhashdc  12925  ctinf  13056  fvsetsid  13121  ressressg  13163  ressabsg  13164  rngplusgg  13225  imasaddvallemg  13403  qusaddvallemg  13421  plusfvalg  13451  mgmb1mgm1  13456  issubmnd  13530  ress0g  13531  imasmnd2  13540  imasmnd  13541  gsumfzz  13583  grpasscan2  13652  grpidrcan  13653  grpidlcan  13654  grpinvadd  13666  grpsubeq0  13674  grppncan  13679  dfgrp3mlem  13686  dfgrp3me  13688  grpsubpropd2  13693  pwsinvg  13700  imasgrp2  13702  imasgrp  13703  mhmmnd  13708  mulgnn0p1  13725  mulgnnsubcl  13726  mulgnn0subcl  13727  mulgsubcl  13728  mulgneg  13732  mulgaddcom  13738  mulginvcom  13739  submmulg  13758  subgcl  13776  subgsubcl  13777  subgsub  13778  subgmulg  13780  nsgconj  13798  nsgid  13807  quseccl0g  13823  ghmmulg  13848  ghmeqker  13863  f1ghm0to0  13864  kerf1ghm  13866  ablinvadd  13902  ablsub4  13905  ablpncan2  13908  subgabl  13924  gsumfzconst  13933  rngcl  13963  imasrng  13975  srgcl  13989  ringcl  14032  crngcom  14033  ringidss  14048  ringcom  14050  imasring  14083  opprringbg  14099  unitmulcl  14133  unitmulclb  14134  dvrcl  14155  unitdvcl  14156  dvrcan1  14160  dvrcan3  14161  rhmmul  14184  subrngrng  14222  subrngmcl  14229  subrgmcl  14253  subrgdv  14258  rrgeq0  14285  domneq0  14292  islmod  14311  scafvalg  14327  lmodcom  14353  rmodislmodlem  14370  rmodislmod  14371  lssclg  14384  lssvnegcl  14396  lssintclm  14404  lspss  14419  lspun  14422  lspsnvsi  14438  rspssp  14514  rnglidlmmgm  14516  rnglidlmsgrp  14517  rnglidlrng  14518  zndvds  14669  2basgeng  14812  iuncld  14845  ntrss  14849  restco  14904  restabs  14905  cnprcl2k  14936  lmconst  14946  cnrest2  14966  cnmpt2t  15023  psmetsym  15059  psmetge0  15061  xmetge0  15095  xmetsym  15098  blvalps  15118  blval  15119  xblcntrps  15143  xblcntr  15144  xmssym  15199  blsscls2  15223  bdxmet  15231  txmetcnp  15248  dvfvalap  15411  dvid  15425  dvidre  15427  dvcnp2cntop  15429  elplyr  15470  rpcxpadd  15635  rpcxpsub  15638  rpmulcxp  15639  rpdivcxp  15641  cxpmul  15642  rpcxple2  15648  rpcxplt2  15649  rplogbval  15675  rplogbcl  15676  rplogbreexp  15683  relogbexpap  15688  logbleb  15691  logblt  15692  rplogbcxp  15693  rpcxplogb  15694  relogbcxpbap  15695  sgmppw  15722  lgsneg1  15760  lgsmod  15761  lgsne0  15773  lgssq  15775  lgsdirnn0  15782  lgsdinn0  15783  lgsquad  15815  funvtxvalg  15893  funiedgvalg  15894  lpvtx  15936  ausgrumgrien  16027  ausgrusgrien  16028  uhgrissubgr  16118  egrsubgr  16120  subumgredg2en  16128  subusgr  16132  wlkl1loop  16215  clwwlknonex2  16296  eulerpathprum  16337  eulerpathum  16338  findset  16566  gfsumsn  16712