Theorem simp2 1029

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl2  1032  simpr2  1035  simp2i  1038  simp2d  1041  simp12  1059  simp22  1062  simp32  1065  syld3an3  1323  3ianorr  1350  intn3an2d  1398  stoic4b  1482  nlim0  4541  tfisi  4736  sotri2  5188  sotri3  5189  feq123  5528  sefvex  5719  fvmptt  5800  fnfvima  5956  cocan1  5996  cocan2  5997  ovexg  6122  ovmpox  6220  ovmpoga  6221  fvmpopr2d  6228  caovimo  6286  suppval1  6483  suppimacnvfn  6490  suppfnss  6501  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfrcllembxssdm  6632  tfrcllembfn  6633  freccllem  6678  frecfcllem  6680  frecsuclem  6682  frecrdg  6684  mapm  6975  domssr  7070  mapxpen  7154  dif1en  7189  diffifi  7204  unsnfidcex  7233  unfidisj  7235  undifdc  7237  resfnfinfinss  7259  funrnfi  7262  fissfi  7269  sbthlemi9  7289  elfir  7312  difinfsn  7446  ctssdc  7459  djuassen  7579  xpdjuen  7580  mulcanenq  7758  ltanqg  7773  mulcanenq0ec  7818  addnnnq0  7822  distrprg  7961  aptipr  8014  addsrpr  8118  mulsrpr  8119  mulasssrg  8131  ltpsrprg  8176  axmulass  8246  axpre-ltadd  8259  subadd2  8537  nppcan  8555  nppcan3  8557  subsub2  8561  subsub4  8566  npncan3  8571  pnpcan  8572  pnncan  8574  subcan  8588  ltadd1  8764  leadd1  8765  leadd2  8766  ltsubadd  8767  ltsubadd2  8768  lesubadd  8769  lesubadd2  8770  ltaddsub  8771  leaddsub  8773  lesub1  8791  lesub2  8792  ltsub1  8793  ltsub2  8794  gt0add  8909  apreap  8923  lemul1  8929  reapmul1lem  8930  reapmul1  8931  reapadd1  8932  remulext1  8935  remulext2  8936  apadd2  8945  mulext2  8949  mulap0r  8951  leltap  8961  ltap  8969  apsub1  8978  recexaplem2  8988  mulcanap  9001  mulcanap2  9002  divvalap  9012  divmulap  9013  divcanap1  9019  diveqap0  9020  divap0b  9021  divrecap  9026  divassap  9028  div23ap  9029  divdirap  9035  divcanap3  9036  div11ap  9038  diveqap1  9043  divmuldivap  9050  divcanap5  9052  redivclap  9069  div2negap  9073  apmul1  9126  apmul2  9127  div2subap  9175  ltdiv1  9206  ledivmul  9215  lemuldiv  9219  lt2msq1  9223  ltdiv23  9230  squeeze0  9242  ofsubeq0  9300  ofnegsub  9301  ind1  9309  zaddcllemneg  9692  zfidc  9732  eluzsub  9967  nn01to3  10032  rpgecl  10099  addlelt  10185  xleadd1  10293  xltadd1  10294  lbioog  10331  ubioc1  10347  ubicc2  10403  icoshftf1o  10409  fzen  10463  nelfzo  10575  ubmelfzo  10634  ssfzo12  10658  ubmelm1fzo  10660  fzosplitprm1  10669  zsupssdc  10689  rebtwn2zlemshrink  10704  qbtwnre  10707  icogelb  10716  flqwordi  10743  flqword2  10744  flltdivnn0lt  10759  modqcl  10783  mulqmod0  10787  modqmulnn  10799  modqabs2  10815  modqmuladdnn0  10825  qnegmod  10826  addmodid  10829  modqm1p1mod0  10832  modifeq2int  10843  modqdi  10849  modqeqmodmin  10851  modfzo0difsn  10852  frec2uzf1od  10863  exp3val  10998  expnegap0  11004  expgt1  11034  exprecap  11037  expmulzap  11042  leexp2a  11049  expubnd  11053  mulbinom2  11113  bernneq2  11119  expnbnd  11121  fihashss  11278  fihashssdif  11280  fimaxq  11291  ccatval2  11387  ccatass  11397  ccatw2s1leng  11427  ccat2s1fvwd  11436  swrdval  11441  swrdnd  11452  pfxfv  11477  pfxpfx  11501  ccats1pfxeq  11507  ccats1pfxeqrex  11508  s3cl  11579  s3fv0g  11584  s3fv1g  11585  s3fv2g  11586  shftuz  11603  shftfibg  11606  cjdivap  11696  resqrtcl  11816  absdivap  11857  abssubne0  11879  maxleast  12001  lemininf  12023  ltmininf  12024  xrmaxltsup  12048  xrmaxaddlem  12050  xrmaxadd  12051  xrmineqinf  12059  xrltmininf  12060  xrminltinf  12062  xrminadd  12065  climuni  12083  reccn2ap  12103  isumz  12180  geoisum1c  12311  prod1dc  12377  efltim  12489  dvdsval2  12581  dvdscmulr  12611  dvdsmulcr  12612  modmulconst  12614  dvdsadd2b  12631  dvdsexp  12652  mulmoddvds  12654  divalglemeuneg  12714  gcdaddm  12785  dvdsgcdb  12814  mulgcd  12817  gcddiv  12820  uzwodc  12838  lcmdvdsb  12886  mulgcddvds  12896  qredeq  12898  divgcdcoprm0  12903  cncongr1  12905  euclemma  12949  rpexp  12956  rpexp12i  12958  fermltl  13040  prmdiv  13041  odzcllem  13049  odzdvds  13052  odzphi  13053  vfermltl  13058  coprimeprodsq  13064  pythagtriplem6  13077  pythagtriplem7  13078  pythagtriplem12  13082  pythagtriplem13  13083  pceu  13102  pcdvdsb  13127  pcgcd1  13135  dvdsprmpweq  13142  sumhashdc  13154  ctinf  13378  fvsetsid  13443  ressressg  13487  ressabsg  13488  rngplusgg  13549  imasaddvallemg  13694  qusaddvallemg  13712  plusfvalg  13741  mgmb1mgm1  13746  issubmnd  13813  ress0g  13814  imasmnd2  13817  imasmnd  13818  grpasscan2  13927  grpidrcan  13928  grpidlcan  13929  grpinvadd  13941  grpsubeq0  13949  grppncan  13954  dfgrp3mlem  13961  dfgrp3me  13963  grpsubpropd2  13968  imasgrp2  13971  imasgrp  13972  mhmmnd  13977  mulgnn0p1  13994  mulgnnsubcl  13995  mulgnn0subcl  13996  mulgsubcl  13997  mulgneg  14001  mulgaddcom  14007  mulginvcom  14008  submmulg  14027  subgcl  14045  subgsubcl  14046  subgsub  14047  subgmulg  14049  nsgconj  14067  nsgid  14076  quseccl0g  14092  ghmmulg  14117  ghmeqker  14132  f1ghm0to0  14133  kerf1ghm  14135  ablinvadd  14203  ablsub4  14206  ablpncan2  14209  subgabl  14225  gzsumconst  14232  gsumsncmn  14245  gsumconstcmn  14265  pwsinvg  14321  rngcl  14349  imasrng  14361  srgcl  14380  ringcl  14423  crngcom  14424  ringidss  14440  ringcom  14442  imasring  14477  opprringbg  14493  unitmulcl  14528  unitmulclb  14529  dvrcl  14550  unitdvcl  14551  dvrcan1  14555  dvrcan3  14556  rhmmul  14579  subrngrng  14618  subrngmcl  14625  subrgmcl  14649  subrgdv  14654  rrgeq0  14681  domneq0  14689  islmod  14735  scafvalg  14752  lmodcom  14778  rmodislmodlem  14795  rmodislmod  14796  lssclg  14809  lssvnegcl  14821  lssintclm  14829  lspss  14844  lspun  14847  lspsnvsi  14863  rspssp  14939  rnglidlmmgm  14941  rnglidlmsgrp  14942  rnglidlrng  14943  zndvds  15092  aspss  15127  asclmul1  15137  asclmul2  15138  ascldimul  15139  asclinvg  15140  asclmulg  15152  psrbagdceq  15167  psrbaglecl  15172  psrbagcon  15174  psrringfi  15213  2basgeng  15325  iuncld  15358  ntrss  15362  restco  15417  restabs  15418  cnprcl2k  15449  lmconst  15459  cnrest2  15479  cnmpt2t  15536  psmetsym  15572  psmetge0  15574  xmetge0  15608  xmetsym  15611  blvalps  15631  blval  15632  xblcntrps  15656  xblcntr  15657  xmssym  15712  blsscls2  15736  bdxmet  15744  txmetcnp  15761  dvfvalap  15924  dvid  15938  dvidre  15940  dvcnp2cntop  15942  elplyr  15983  logfac  16143  rpcxpadd  16155  rpcxpsub  16158  rpmulcxp  16159  rpdivcxp  16161  cxpmul  16162  rpcxple2  16170  rpcxplt2  16171  rplogbval  16198  rplogbcl  16199  rplogbreexp  16206  relogbexpap  16211  logbleb  16214  logblt  16215  rplogbcxp  16216  rpcxplogb  16217  relogbcxpbap  16218  sgmppw  16303  bcmono  16321  prmefexple  16325  lgsneg1  16366  lgsmod  16367  lgsne0  16379  lgssq  16381  lgsdirnn0  16388  lgsdinn0  16389  lgsquad  16421  funvtxvalg  16499  funiedgvalg  16500  lpvtx  16542  ausgrumgrien  16633  ausgrusgrien  16634  uhgrissubgr  16724  egrsubgr  16726  subumgredg2en  16734  subusgr  16738  wlkl1loop  16821  clwwlknonex2  16902  eulerpathprum  16943  eulerpathum  16944  findset  17193  repiecele0  17298  repiecege0  17299