Theorem simp2 993

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

Syntax hints:   -> wi 4   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  simpl2  996  simpr2  999  simp2i  1002  simp2d  1005  simp12  1023  simp22  1026  simp32  1029  syld3an3  1278  3ianorr  1304  stoic4b  1426  nlim0  4379  tfisi  4571  sotri2  5008  sotri3  5009  feq123  5339  sefvex  5517  fvmptt  5587  fnfvima  5730  cocan1  5766  cocan2  5767  ovexg  5887  ovmpox  5981  ovmpoga  5982  caovimo  6046  tfr1onlembxssdm  6322  tfr1onlembfn  6323  tfrcllembxssdm  6335  tfrcllembfn  6336  freccllem  6381  frecfcllem  6383  frecsuclem  6385  frecrdg  6387  mapxpen  6826  dif1en  6857  diffifi  6872  unsnfidcex  6897  unfidisj  6899  undifdc  6901  resfnfinfinss  6917  funrnfi  6919  sbthlemi9  6942  elfir  6950  difinfsn  7077  ctssdc  7090  djuassen  7194  xpdjuen  7195  mulcanenq  7347  ltanqg  7362  mulcanenq0ec  7407  addnnnq0  7411  distrprg  7550  aptipr  7603  addsrpr  7707  mulsrpr  7708  mulasssrg  7720  ltpsrprg  7765  axmulass  7835  axpre-ltadd  7848  subadd2  8123  nppcan  8141  nppcan3  8143  subsub2  8147  subsub4  8152  npncan3  8157  pnpcan  8158  pnncan  8160  subcan  8174  ltadd1  8348  leadd1  8349  leadd2  8350  ltsubadd  8351  ltsubadd2  8352  lesubadd  8353  lesubadd2  8354  ltaddsub  8355  leaddsub  8357  lesub1  8375  lesub2  8376  ltsub1  8377  ltsub2  8378  gt0add  8492  apreap  8506  lemul1  8512  reapmul1lem  8513  reapmul1  8514  reapadd1  8515  remulext1  8518  remulext2  8519  apadd2  8528  mulext2  8532  mulap0r  8534  leltap  8544  ltap  8552  apsub1  8561  recexaplem2  8570  mulcanap  8583  mulcanap2  8584  divvalap  8591  divmulap  8592  divcanap1  8598  diveqap0  8599  divap0b  8600  divrecap  8605  divassap  8607  div23ap  8608  divdirap  8614  divcanap3  8615  div11ap  8617  diveqap1  8622  divmuldivap  8629  divcanap5  8631  redivclap  8648  div2negap  8652  apmul1  8705  apmul2  8706  div2subap  8754  ltdiv1  8784  ledivmul  8793  lemuldiv  8797  lt2msq1  8801  ltdiv23  8808  squeeze0  8820  zaddcllemneg  9251  eluzsub  9516  nn01to3  9576  rpgecl  9639  addlelt  9725  xleadd1  9832  xltadd1  9833  lbioog  9870  ubioc1  9886  ubicc2  9942  icoshftf1o  9948  fzen  9999  ubmelfzo  10156  ssfzo12  10180  ubmelm1fzo  10182  fzosplitprm1  10190  rebtwn2zlemshrink  10210  qbtwnre  10213  icogelb  10222  flqwordi  10244  flqword2  10245  flltdivnn0lt  10260  modqcl  10282  mulqmod0  10286  modqmulnn  10298  modqabs2  10314  modqmuladdnn0  10324  qnegmod  10325  addmodid  10328  modqm1p1mod0  10331  modifeq2int  10342  modqdi  10348  modqeqmodmin  10350  modfzo0difsn  10351  frec2uzf1od  10362  exp3val  10478  expnegap0  10484  expgt1  10514  exprecap  10517  expmulzap  10522  leexp2a  10529  expubnd  10533  mulbinom2  10592  bernneq2  10597  expnbnd  10599  fihashss  10751  fihashssdif  10753  fimaxq  10762  shftuz  10781  shftfibg  10784  cjdivap  10873  resqrtcl  10993  absdivap  11034  abssubne0  11055  maxleast  11177  lemininf  11197  ltmininf  11198  xrmaxltsup  11221  xrmaxaddlem  11223  xrmaxadd  11224  xrmineqinf  11232  xrltmininf  11233  xrminltinf  11235  xrminadd  11238  climuni  11256  reccn2ap  11276  isumz  11352  geoisum1c  11483  prod1dc  11549  efltim  11661  dvdsval2  11752  dvdscmulr  11782  dvdsmulcr  11783  modmulconst  11785  dvdsadd2b  11802  dvdsexp  11821  mulmoddvds  11823  divalglemeuneg  11882  zsupssdc  11909  gcdaddm  11939  dvdsgcdb  11968  mulgcd  11971  gcddiv  11974  uzwodc  11992  lcmdvdsb  12038  mulgcddvds  12048  qredeq  12050  divgcdcoprm0  12055  cncongr1  12057  euclemma  12100  rpexp  12107  rpexp12i  12109  fermltl  12188  prmdiv  12189  odzcllem  12196  odzdvds  12199  odzphi  12200  vfermltl  12205  coprimeprodsq  12211  pythagtriplem6  12224  pythagtriplem7  12225  pythagtriplem12  12229  pythagtriplem13  12230  pceu  12249  pcdvdsb  12273  pcgcd1  12281  dvdsprmpweq  12288  sumhashdc  12299  ctinf  12385  fvsetsid  12450  ressid2  12477  ressval2  12478  rngplusgg  12535  plusfvalg  12617  mgmb1mgm1  12622  grpasscan2  12763  grpidrcan  12764  grpidlcan  12765  2basgeng  12876  iuncld  12909  ntrss  12913  restco  12968  restabs  12969  cnprcl2k  13000  lmconst  13010  cnrest2  13030  cnmpt2t  13087  psmetsym  13123  psmetge0  13125  xmetge0  13159  xmetsym  13162  blvalps  13182  blval  13183  xblcntrps  13207  xblcntr  13208  xmssym  13263  blsscls2  13287  bdxmet  13295  txmetcnp  13312  dvfvalap  13444  dvid  13456  dvcnp2cntop  13457  rpcxpadd  13620  rpcxpsub  13623  rpmulcxp  13624  rpdivcxp  13626  cxpmul  13627  rpcxple2  13632  rpcxplt2  13633  rplogbval  13657  rplogbcl  13658  rplogbreexp  13665  relogbexpap  13670  logbleb  13673  logblt  13674  rplogbcxp  13675  rpcxplogb  13676  relogbcxpbap  13677  lgsneg1  13720  lgsmod  13721  lgsne0  13733  lgssq  13735  lgsdirnn0  13742  lgsdinn0  13743  findset  13980