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  4539  tfisi  4734  sotri2  5185  sotri3  5186  feq123  5525  sefvex  5716  fvmptt  5797  fnfvima  5953  cocan1  5993  cocan2  5994  ovexg  6119  ovmpox  6217  ovmpoga  6218  fvmpopr2d  6225  caovimo  6283  suppval1  6479  suppimacnvfn  6486  suppfnss  6497  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfrcllembxssdm  6627  tfrcllembfn  6628  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecrdg  6679  domssr  7064  mapxpen  7148  dif1en  7183  diffifi  7198  unsnfidcex  7227  unfidisj  7229  undifdc  7231  resfnfinfinss  7253  funrnfi  7256  fissfi  7263  sbthlemi9  7282  elfir  7307  difinfsn  7440  ctssdc  7453  djuassen  7573  xpdjuen  7574  mulcanenq  7752  ltanqg  7767  mulcanenq0ec  7812  addnnnq0  7816  distrprg  7955  aptipr  8008  addsrpr  8112  mulsrpr  8113  mulasssrg  8125  ltpsrprg  8170  axmulass  8240  axpre-ltadd  8253  subadd2  8530  nppcan  8548  nppcan3  8550  subsub2  8554  subsub4  8559  npncan3  8564  pnpcan  8565  pnncan  8567  subcan  8581  ltadd1  8757  leadd1  8758  leadd2  8759  ltsubadd  8760  ltsubadd2  8761  lesubadd  8762  lesubadd2  8763  ltaddsub  8764  leaddsub  8766  lesub1  8784  lesub2  8785  ltsub1  8786  ltsub2  8787  gt0add  8901  apreap  8915  lemul1  8921  reapmul1lem  8922  reapmul1  8923  reapadd1  8924  remulext1  8927  remulext2  8928  apadd2  8937  mulext2  8941  mulap0r  8943  leltap  8953  ltap  8961  apsub1  8970  recexaplem2  8980  mulcanap  8993  mulcanap2  8994  divvalap  9004  divmulap  9005  divcanap1  9011  diveqap0  9012  divap0b  9013  divrecap  9018  divassap  9020  div23ap  9021  divdirap  9027  divcanap3  9028  div11ap  9030  diveqap1  9035  divmuldivap  9042  divcanap5  9044  redivclap  9061  div2negap  9065  apmul1  9118  apmul2  9119  div2subap  9167  ltdiv1  9198  ledivmul  9207  lemuldiv  9211  lt2msq1  9215  ltdiv23  9222  squeeze0  9234  ofnegsub  9292  ind1  9300  zaddcllemneg  9683  zfidc  9723  eluzsub  9952  nn01to3  10017  rpgecl  10083  addlelt  10169  xleadd1  10277  xltadd1  10278  lbioog  10315  ubioc1  10331  ubicc2  10387  icoshftf1o  10393  fzen  10447  nelfzo  10559  ubmelfzo  10618  ssfzo12  10642  ubmelm1fzo  10644  fzosplitprm1  10653  zsupssdc  10673  rebtwn2zlemshrink  10688  qbtwnre  10691  icogelb  10700  flqwordi  10723  flqword2  10724  flltdivnn0lt  10739  modqcl  10763  mulqmod0  10767  modqmulnn  10779  modqabs2  10795  modqmuladdnn0  10805  qnegmod  10806  addmodid  10809  modqm1p1mod0  10812  modifeq2int  10823  modqdi  10829  modqeqmodmin  10831  modfzo0difsn  10832  frec2uzf1od  10843  exp3val  10978  expnegap0  10984  expgt1  11014  exprecap  11017  expmulzap  11022  leexp2a  11029  expubnd  11033  mulbinom2  11093  bernneq2  11099  expnbnd  11101  fihashss  11257  fihashssdif  11259  fimaxq  11270  ccatval2  11366  ccatass  11376  ccatw2s1leng  11406  ccat2s1fvwd  11415  swrdval  11420  swrdnd  11431  pfxfv  11456  pfxpfx  11480  ccats1pfxeq  11486  ccats1pfxeqrex  11487  s3cl  11558  s3fv0g  11563  s3fv1g  11564  s3fv2g  11565  shftuz  11582  shftfibg  11585  cjdivap  11675  resqrtcl  11795  absdivap  11836  abssubne0  11857  maxleast  11979  lemininf  12000  ltmininf  12001  xrmaxltsup  12024  xrmaxaddlem  12026  xrmaxadd  12027  xrmineqinf  12035  xrltmininf  12036  xrminltinf  12038  xrminadd  12041  climuni  12059  reccn2ap  12079  isumz  12156  geoisum1c  12287  prod1dc  12353  efltim  12465  dvdsval2  12557  dvdscmulr  12587  dvdsmulcr  12588  modmulconst  12590  dvdsadd2b  12607  dvdsexp  12628  mulmoddvds  12630  divalglemeuneg  12690  gcdaddm  12761  dvdsgcdb  12790  mulgcd  12793  gcddiv  12796  uzwodc  12814  lcmdvdsb  12862  mulgcddvds  12872  qredeq  12874  divgcdcoprm0  12879  cncongr1  12881  euclemma  12924  rpexp  12931  rpexp12i  12933  fermltl  13012  prmdiv  13013  odzcllem  13021  odzdvds  13024  odzphi  13025  vfermltl  13030  coprimeprodsq  13036  pythagtriplem6  13049  pythagtriplem7  13050  pythagtriplem12  13054  pythagtriplem13  13055  pceu  13074  pcdvdsb  13099  pcgcd1  13107  dvdsprmpweq  13114  sumhashdc  13126  ctinf  13321  fvsetsid  13386  ressressg  13429  ressabsg  13430  rngplusgg  13491  imasaddvallemg  13636  qusaddvallemg  13654  plusfvalg  13683  mgmb1mgm1  13688  issubmnd  13755  ress0g  13756  imasmnd2  13759  imasmnd  13760  grpasscan2  13869  grpidrcan  13870  grpidlcan  13871  grpinvadd  13883  grpsubeq0  13891  grppncan  13896  dfgrp3mlem  13903  dfgrp3me  13905  grpsubpropd2  13910  imasgrp2  13913  imasgrp  13914  mhmmnd  13919  mulgnn0p1  13936  mulgnnsubcl  13937  mulgnn0subcl  13938  mulgsubcl  13939  mulgneg  13943  mulgaddcom  13949  mulginvcom  13950  submmulg  13969  subgcl  13987  subgsubcl  13988  subgsub  13989  subgmulg  13991  nsgconj  14009  nsgid  14018  quseccl0g  14034  ghmmulg  14059  ghmeqker  14074  f1ghm0to0  14075  kerf1ghm  14077  ablinvadd  14114  ablsub4  14117  ablpncan2  14120  subgabl  14136  gzsumconst  14143  gsumsncmn  14156  gsumconstcmn  14166  pwsinvg  14215  rngcl  14243  imasrng  14255  srgcl  14274  ringcl  14317  crngcom  14318  ringidss  14334  ringcom  14336  imasring  14369  opprringbg  14385  unitmulcl  14420  unitmulclb  14421  dvrcl  14442  unitdvcl  14443  dvrcan1  14447  dvrcan3  14448  rhmmul  14471  subrngrng  14510  subrngmcl  14517  subrgmcl  14541  subrgdv  14546  rrgeq0  14573  domneq0  14581  islmod  14627  scafvalg  14644  lmodcom  14670  rmodislmodlem  14687  rmodislmod  14688  lssclg  14701  lssvnegcl  14713  lssintclm  14721  lspss  14736  lspun  14739  lspsnvsi  14755  rspssp  14831  rnglidlmmgm  14833  rnglidlmsgrp  14834  rnglidlrng  14835  zndvds  14984  aspss  15019  asclmul1  15029  asclmul2  15030  ascldimul  15031  asclinvg  15032  asclmulg  15044  psrbaglecl  15060  psrbagcon  15062  2basgeng  15183  iuncld  15216  ntrss  15220  restco  15275  restabs  15276  cnprcl2k  15307  lmconst  15317  cnrest2  15337  cnmpt2t  15394  psmetsym  15430  psmetge0  15432  xmetge0  15466  xmetsym  15469  blvalps  15489  blval  15490  xblcntrps  15514  xblcntr  15515  xmssym  15570  blsscls2  15594  bdxmet  15602  txmetcnp  15619  dvfvalap  15782  dvid  15796  dvidre  15798  dvcnp2cntop  15800  elplyr  15841  logfac  15995  rpcxpadd  16007  rpcxpsub  16010  rpmulcxp  16011  rpdivcxp  16013  cxpmul  16014  rpcxple2  16020  rpcxplt2  16021  rplogbval  16047  rplogbcl  16048  rplogbreexp  16055  relogbexpap  16060  logbleb  16063  logblt  16064  rplogbcxp  16065  rpcxplogb  16066  relogbcxpbap  16067  sgmppw  16106  lgsneg1  16144  lgsmod  16145  lgsne0  16157  lgssq  16159  lgsdirnn0  16166  lgsdinn0  16167  lgsquad  16199  funvtxvalg  16277  funiedgvalg  16278  lpvtx  16320  ausgrumgrien  16411  ausgrusgrien  16412  uhgrissubgr  16502  egrsubgr  16504  subumgredg2en  16512  subusgr  16516  wlkl1loop  16599  clwwlknonex2  16680  eulerpathprum  16721  eulerpathum  16722  findset  16971  repiecele0  17075  repiecege0  17076