Theorem simp2 905

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

Syntax hints:   -> wi 4   /\ w3a 885

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

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  simpl2  908  simpr2  911  simp2i  914  simp2d  917  simp12  935  simp22  938  simp32  941  syld3an3  1180  3ianorr  1204  stoic4b  1322  nlim0  4131  tfisi  4310  sotri2  4722  sotri3  4723  feq123  5038  sefvex  5196  fvmptt  5262  fnfvima  5393  cocan1  5427  cocan2  5428  ovexg  5539  ovmpt2x  5629  ovmpt2ga  5630  caovimo  5694  frecsuclem3  5990  dif1en  6337  diffifi  6351  mulcanenq  6483  ltanqg  6498  mulcanenq0ec  6543  addnnnq0  6547  distrprg  6686  aptipr  6739  addsrpr  6830  mulsrpr  6831  mulasssrg  6843  axmulass  6947  axpre-ltadd  6960  subadd2  7215  nppcan  7233  nppcan3  7235  subsub2  7239  subsub4  7244  npncan3  7249  pnpcan  7250  pnncan  7252  subcan  7266  ltadd1  7424  leadd1  7425  leadd2  7426  ltsubadd  7427  ltsubadd2  7428  lesubadd  7429  lesubadd2  7430  ltaddsub  7431  leaddsub  7433  lesub1  7451  lesub2  7452  ltsub1  7453  ltsub2  7454  gt0add  7564  apreap  7578  lemul1  7584  reapmul1lem  7585  reapmul1  7586  reapadd1  7587  remulext1  7590  remulext2  7591  apadd2  7600  mulext2  7604  mulap0r  7606  leltap  7615  ltap  7622  recexaplem2  7633  mulcanap  7646  mulcanap2  7647  divvalap  7653  divmulap  7654  divcanap1  7660  diveqap0  7661  divap0b  7662  divrecap  7667  divassap  7669  div23ap  7670  divdirap  7674  divcanap3  7675  div11ap  7677  diveqap1  7682  divmuldivap  7688  divcanap5  7690  redivclap  7707  div2negap  7711  apmul1  7764  ltdiv1  7834  ledivmul  7843  lemuldiv  7847  lt2msq1  7851  ltdiv23  7858  squeeze0  7870  zaddcllemneg  8284  eluzsub  8502  nn01to3  8552  rpgecl  8611  lbioog  8782  ubioc1  8798  ubicc2  8853  icoshftf1o  8859  fzen  8907  ubmelfzo  9056  ssfzo12  9080  ubmelm1fzo  9082  fzosplitprm1  9090  qbtwnzlemshrink  9104  rebtwn2zlemshrink  9108  qbtwnre  9111  flqwordi  9130  flqword2  9131  flltdivnn0lt  9146  modqcl  9168  mulqmod0  9172  modqmulnn  9184  frec2uzf1od  9192  expnegap0  9263  expgt1  9293  exprecap  9296  expmulzap  9301  leexp2a  9307  expubnd  9311  bernneq2  9370  expnbnd  9372  shftuz  9418  shftfibg  9421  cjdivap  9509  resqrtcl  9627  absdivap  9668  abssubne0  9687  climuni  9814  findset  10070