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  5888  cocan1  5927  cocan2  5928  ovexg  6051  ovmpox  6149  ovmpoga  6150  fvmpopr2d  6157  caovimo  6215  tfr1onlembxssdm  6508  tfr1onlembfn  6509  tfrcllembxssdm  6521  tfrcllembfn  6522  freccllem  6567  frecfcllem  6569  frecsuclem  6571  frecrdg  6573  domssr  6950  mapxpen  7033  dif1en  7067  diffifi  7082  unsnfidcex  7111  unfidisj  7113  undifdc  7115  resfnfinfinss  7137  funrnfi  7140  sbthlemi9  7163  elfir  7171  difinfsn  7298  ctssdc  7311  djuassen  7431  xpdjuen  7432  mulcanenq  7604  ltanqg  7619  mulcanenq0ec  7664  addnnnq0  7668  distrprg  7807  aptipr  7860  addsrpr  7964  mulsrpr  7965  mulasssrg  7977  ltpsrprg  8022  axmulass  8092  axpre-ltadd  8105  subadd2  8382  nppcan  8400  nppcan3  8402  subsub2  8406  subsub4  8411  npncan3  8416  pnpcan  8417  pnncan  8419  subcan  8433  ltadd1  8608  leadd1  8609  leadd2  8610  ltsubadd  8611  ltsubadd2  8612  lesubadd  8613  lesubadd2  8614  ltaddsub  8615  leaddsub  8617  lesub1  8635  lesub2  8636  ltsub1  8637  ltsub2  8638  gt0add  8752  apreap  8766  lemul1  8772  reapmul1lem  8773  reapmul1  8774  reapadd1  8775  remulext1  8778  remulext2  8779  apadd2  8788  mulext2  8792  mulap0r  8794  leltap  8804  ltap  8812  apsub1  8821  recexaplem2  8831  mulcanap  8844  mulcanap2  8845  divvalap  8853  divmulap  8854  divcanap1  8860  diveqap0  8861  divap0b  8862  divrecap  8867  divassap  8869  div23ap  8870  divdirap  8876  divcanap3  8877  div11ap  8879  diveqap1  8884  divmuldivap  8891  divcanap5  8893  redivclap  8910  div2negap  8914  apmul1  8967  apmul2  8968  div2subap  9016  ltdiv1  9047  ledivmul  9056  lemuldiv  9060  lt2msq1  9064  ltdiv23  9071  squeeze0  9083  ofnegsub  9141  zaddcllemneg  9517  eluzsub  9785  nn01to3  9850  rpgecl  9916  addlelt  10002  xleadd1  10109  xltadd1  10110  lbioog  10147  ubioc1  10163  ubicc2  10219  icoshftf1o  10225  fzen  10277  nelfzo  10386  ubmelfzo  10444  ssfzo12  10468  ubmelm1fzo  10470  fzosplitprm1  10479  zsupssdc  10497  rebtwn2zlemshrink  10512  qbtwnre  10515  icogelb  10524  flqwordi  10547  flqword2  10548  flltdivnn0lt  10563  modqcl  10587  mulqmod0  10591  modqmulnn  10603  modqabs2  10619  modqmuladdnn0  10629  qnegmod  10630  addmodid  10633  modqm1p1mod0  10636  modifeq2int  10647  modqdi  10653  modqeqmodmin  10655  modfzo0difsn  10656  frec2uzf1od  10667  exp3val  10802  expnegap0  10808  expgt1  10838  exprecap  10841  expmulzap  10846  leexp2a  10853  expubnd  10857  mulbinom2  10917  bernneq2  10922  expnbnd  10924  fihashss  11079  fihashssdif  11081  fimaxq  11090  ccatval2  11174  ccatass  11184  ccatw2s1leng  11214  ccat2s1fvwd  11223  swrdval  11228  swrdnd  11239  pfxfv  11264  pfxpfx  11288  ccats1pfxeq  11294  ccats1pfxeqrex  11295  s3cl  11366  s3fv0g  11371  s3fv1g  11372  s3fv2g  11373  shftuz  11377  shftfibg  11380  cjdivap  11469  resqrtcl  11589  absdivap  11630  abssubne0  11651  maxleast  11773  lemininf  11794  ltmininf  11795  xrmaxltsup  11818  xrmaxaddlem  11820  xrmaxadd  11821  xrmineqinf  11829  xrltmininf  11830  xrminltinf  11832  xrminadd  11835  climuni  11853  reccn2ap  11873  isumz  11949  geoisum1c  12080  prod1dc  12146  efltim  12258  dvdsval2  12350  dvdscmulr  12380  dvdsmulcr  12381  modmulconst  12383  dvdsadd2b  12400  dvdsexp  12421  mulmoddvds  12423  divalglemeuneg  12483  gcdaddm  12554  dvdsgcdb  12583  mulgcd  12586  gcddiv  12589  uzwodc  12607  lcmdvdsb  12655  mulgcddvds  12665  qredeq  12667  divgcdcoprm0  12672  cncongr1  12674  euclemma  12717  rpexp  12724  rpexp12i  12726  fermltl  12805  prmdiv  12806  odzcllem  12814  odzdvds  12817  odzphi  12818  vfermltl  12823  coprimeprodsq  12829  pythagtriplem6  12842  pythagtriplem7  12843  pythagtriplem12  12847  pythagtriplem13  12848  pceu  12867  pcdvdsb  12892  pcgcd1  12900  dvdsprmpweq  12907  sumhashdc  12919  ctinf  13050  fvsetsid  13115  ressressg  13157  ressabsg  13158  rngplusgg  13219  imasaddvallemg  13397  qusaddvallemg  13415  plusfvalg  13445  mgmb1mgm1  13450  issubmnd  13524  ress0g  13525  imasmnd2  13534  imasmnd  13535  gsumfzz  13577  grpasscan2  13646  grpidrcan  13647  grpidlcan  13648  grpinvadd  13660  grpsubeq0  13668  grppncan  13673  dfgrp3mlem  13680  dfgrp3me  13682  grpsubpropd2  13687  pwsinvg  13694  imasgrp2  13696  imasgrp  13697  mhmmnd  13702  mulgnn0p1  13719  mulgnnsubcl  13720  mulgnn0subcl  13721  mulgsubcl  13722  mulgneg  13726  mulgaddcom  13732  mulginvcom  13733  submmulg  13752  subgcl  13770  subgsubcl  13771  subgsub  13772  subgmulg  13774  nsgconj  13792  nsgid  13801  quseccl0g  13817  ghmmulg  13842  ghmeqker  13857  f1ghm0to0  13858  kerf1ghm  13860  ablinvadd  13896  ablsub4  13899  ablpncan2  13902  subgabl  13918  gsumfzconst  13927  rngcl  13956  imasrng  13968  srgcl  13982  ringcl  14025  crngcom  14026  ringidss  14041  ringcom  14043  imasring  14076  opprringbg  14092  unitmulcl  14126  unitmulclb  14127  dvrcl  14148  unitdvcl  14149  dvrcan1  14153  dvrcan3  14154  rhmmul  14177  subrngrng  14215  subrngmcl  14222  subrgmcl  14246  subrgdv  14251  rrgeq0  14278  domneq0  14285  islmod  14304  scafvalg  14320  lmodcom  14346  rmodislmodlem  14363  rmodislmod  14364  lssclg  14377  lssvnegcl  14389  lssintclm  14397  lspss  14412  lspun  14415  lspsnvsi  14431  rspssp  14507  rnglidlmmgm  14509  rnglidlmsgrp  14510  rnglidlrng  14511  zndvds  14662  2basgeng  14805  iuncld  14838  ntrss  14842  restco  14897  restabs  14898  cnprcl2k  14929  lmconst  14939  cnrest2  14959  cnmpt2t  15016  psmetsym  15052  psmetge0  15054  xmetge0  15088  xmetsym  15091  blvalps  15111  blval  15112  xblcntrps  15136  xblcntr  15137  xmssym  15192  blsscls2  15216  bdxmet  15224  txmetcnp  15241  dvfvalap  15404  dvid  15418  dvidre  15420  dvcnp2cntop  15422  elplyr  15463  rpcxpadd  15628  rpcxpsub  15631  rpmulcxp  15632  rpdivcxp  15634  cxpmul  15635  rpcxple2  15641  rpcxplt2  15642  rplogbval  15668  rplogbcl  15669  rplogbreexp  15676  relogbexpap  15681  logbleb  15684  logblt  15685  rplogbcxp  15686  rpcxplogb  15687  relogbcxpbap  15688  sgmppw  15715  lgsneg1  15753  lgsmod  15754  lgsne0  15766  lgssq  15768  lgsdirnn0  15775  lgsdinn0  15776  lgsquad  15808  funvtxvalg  15886  funiedgvalg  15887  lpvtx  15929  ausgrumgrien  16020  ausgrusgrien  16021  uhgrissubgr  16111  egrsubgr  16113  subumgredg2en  16121  subusgr  16125  wlkl1loop  16208  clwwlknonex2  16289  findset  16540