Theorem simpr3 1029

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

Assertion

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

Proof of Theorem simpr3

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1002

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

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  simplr3  1065  simprr3  1071  simp1r3  1119  simp2r3  1125  simp3r3  1131  3anandis  1381  isopolem  5952  tfrlemibacc  6478  tfrlemibxssdm  6479  tfrlemibfn  6480  tfr1onlembacc  6494  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfrcllembacc  6507  tfrcllembxssdm  6508  tfrcllembfn  6509  elfir  7151  prloc  7689  prmuloc2  7765  ltntri  8285  eluzuzle  9742  xlesubadd  10091  elioc2  10144  elico2  10145  elicc2  10146  fseq1p1m1  10302  seq3f1olemp  10749  seq3f1oleml  10750  bcval5  10997  hashdifpr  11055  ccatswrd  11217  pfxccat3a  11285  isumss2  11919  tanaddap  12265  dvds2ln  12350  divalglemeunn  12447  divalglemex  12448  divalglemeuneg  12449  f1ovscpbl  13360  prdssgrpd  13463  prdsmndd  13496  imasmnd2  13500  imasmnd  13501  grpsubadd  13636  grpaddsubass  13638  grpsubsub4  13641  grppnpcan2  13642  grpnpncan  13643  grpnnncan2  13645  imasgrp2  13662  imasgrp  13663  mulgnndir  13703  mulgnn0dir  13704  mulgnnass  13709  mulgnn0ass  13710  mulgass  13711  issubg2m  13741  qusgrp  13784  kerf1ghm  13826  cmn32  13856  cmn12  13858  abladdsub  13867  ablsubsub23  13877  rngass  13917  imasrng  13934  srgdilem  13947  srgass  13949  ringdilem  13990  ringass  13994  ringrng  14014  imasring  14042  opprrng  14055  opprring  14057  mulgass3  14063  unitgrp  14095  dvrass  14118  dvrdir  14122  subrgunit  14218  issubrg2  14220  aprap  14265  lss1  14341  lsssn0  14349  islss3  14358  sralmod  14429  restopnb  14870  icnpimaex  14900  cnptopresti  14927  psmettri  15019  isxmet2d  15037  xmettri  15061  metrtri  15066  xmetres2  15068  bldisj  15090  blss2ps  15095  blss2  15096  xmstri2  15159  mstri2  15160  xmstri  15161  mstri  15162  xmstri3  15163  mstri3  15164  msrtri  15165  comet  15188  bdbl  15192  xmetxp  15196  dvconst  15383  dvconstre  15385  dvconstss  15387  sgmmul  15685  pw1ndom3  16413