Theorem simpr3 1007

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 1001	. 2 |- ( ( ps /\ ch /\ th ) -> th )
2	1	adantl 277	1 |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> th )

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

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 982

This theorem is referenced by:  simplr3  1043  simprr3  1049  simp1r3  1097  simp2r3  1103  simp3r3  1109  3anandis  1358  isopolem  5844  tfrlemibacc  6351  tfrlemibxssdm  6352  tfrlemibfn  6353  tfr1onlembacc  6367  tfr1onlembxssdm  6368  tfr1onlembfn  6369  tfrcllembacc  6380  tfrcllembxssdm  6381  tfrcllembfn  6382  elfir  7002  prloc  7520  prmuloc2  7596  ltntri  8115  eluzuzle  9566  xlesubadd  9913  elioc2  9966  elico2  9967  elicc2  9968  fseq1p1m1  10124  seq3f1olemp  10533  seq3f1oleml  10534  bcval5  10775  hashdifpr  10832  isumss2  11433  tanaddap  11779  dvds2ln  11863  divalglemeunn  11958  divalglemex  11959  divalglemeuneg  11960  f1ovscpbl  12789  grpsubadd  13032  grpaddsubass  13034  grpsubsub4  13037  grppnpcan2  13038  grpnpncan  13039  grpnnncan2  13041  imasgrp2  13052  imasgrp  13053  mulgnndir  13091  mulgnn0dir  13092  mulgnnass  13097  mulgnn0ass  13098  mulgass  13099  issubg2m  13128  qusgrp  13171  kerf1ghm  13213  cmn32  13243  cmn12  13245  abladdsub  13254  ablsubsub23  13264  rngass  13293  imasrng  13310  srgdilem  13323  srgass  13325  ringdilem  13366  ringass  13370  ringrng  13390  imasring  13414  opprrng  13427  opprring  13429  mulgass3  13435  unitgrp  13466  dvrass  13489  dvrdir  13493  subrgunit  13586  issubrg2  13588  aprap  13602  lss1  13678  lsssn0  13686  islss3  13695  sralmod  13766  restopnb  14141  icnpimaex  14171  cnptopresti  14198  psmettri  14290  isxmet2d  14308  xmettri  14332  metrtri  14337  xmetres2  14339  bldisj  14361  blss2ps  14366  blss2  14367  xmstri2  14430  mstri2  14431  xmstri  14432  mstri  14433  xmstri3  14434  mstri3  14435  msrtri  14436  comet  14459  bdbl  14463  xmetxp  14467  dvconst  14621