Theorem simpr2 1035

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpr2	|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ch )

Proof of Theorem simpr2

Step	Hyp	Ref	Expression
1		simp2 1029	. 2 |- ( ( ps /\ ch /\ th ) -> ch )
2	1	adantl 277	1 |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ch )

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

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

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

This theorem is used by:  simplr2  1071  simprr2  1077  simp1r2  1125  simp2r2  1131  simp3r2  1137  3anandis  1388  isopolem  6028  tfrlemibacc  6597  tfrlemibfn  6599  tfr1onlembacc  6613  tfr1onlembfn  6615  tfrcllembacc  6626  tfrcllembfn  6628  prltlu  7854  prdisj  7859  prmuloc2  7934  ltntri  8455  eluzuzle  9939  xlesubadd  10295  elioc2  10348  elico2  10349  elicc2  10350  fseq1p1m1  10511  fz0fzelfz0  10544  seq3f1olemp  10965  bcval5  11215  hashdifpr  11275  hashtpgim  11311  swrdsbslen  11452  ccatswrd  11456  swrdswrdlem  11490  summodclem2  12165  isumss2  12176  tanaddap  12522  dvds2ln  12607  divalglemeunn  12704  divalglemex  12705  divalglemeuneg  12706  isstructr  13416  f1ovscpbl  13682  mndissubm  13831  grpsubrcan  13935  grpsubadd  13942  grpaddsubass  13944  grpsubsub4  13947  grppnpcan2  13948  grpnpncan  13949  mulgnndir  14003  mulgnn0dir  14004  mulgdir  14006  mulgnnass  14009  mulgnn0ass  14010  mulgass  14011  mulgsubdir  14014  issubg2m  14041  eqgval  14075  qusgrp  14084  cmn32  14156  cmn12  14158  abladdsub  14168  ablsubsub23  14178  prdssgrpd  14240  prdsmndd  14243  rngass  14287  srgdilem  14322  srgass  14324  ringdilem  14365  ringass  14369  opprrng  14431  opprring  14433  mulgass3  14440  unitgrp  14472  dvrass  14495  dvrdir  14499  subrgunit  14596  issubrg2  14598  aprap  14647  lsssn0  14756  islss3  14765  sralmod  14836  restopnb  15331  icnpimaex  15361  cnptopresti  15388  psmettri  15480  isxmet2d  15498  xmettri  15522  metrtri  15527  xmetres2  15529  bldisj  15551  blss2ps  15556  blss2  15557  xmstri2  15620  mstri2  15621  xmstri  15622  mstri  15623  xmstri3  15624  mstri3  15625  msrtri  15626  comet  15649  bdbl  15653  xmetxp  15657  dvconst  15844  dvconstre  15846  dvconstss  15848  sgmmul  16191  gausslemma2dlem1a  16275  pw1ndom3  17118