Theorem simpr3 1032

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

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

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 1007

This theorem is referenced by:  simplr3  1068  simprr3  1074  simp1r3  1122  simp2r3  1128  simp3r3  1134  3anandis  1384  isopolem  5973  suppfnss  6435  tfrlemibacc  6535  tfrlemibxssdm  6536  tfrlemibfn  6537  tfr1onlembacc  6551  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfrcllembacc  6564  tfrcllembxssdm  6565  tfrcllembfn  6566  elfir  7215  prloc  7754  prmuloc2  7830  ltntri  8349  eluzuzle  9808  xlesubadd  10162  elioc2  10215  elico2  10216  elicc2  10217  fseq1p1m1  10374  seq3f1olemp  10823  seq3f1oleml  10824  bcval5  11071  hashdifpr  11130  hashtpgim  11155  ccatswrd  11300  pfxccat3a  11368  isumss2  12017  tanaddap  12363  dvds2ln  12448  divalglemeunn  12545  divalglemex  12546  divalglemeuneg  12547  f1ovscpbl  13458  prdssgrpd  13561  prdsmndd  13594  imasmnd2  13598  imasmnd  13599  grpsubadd  13734  grpaddsubass  13736  grpsubsub4  13739  grppnpcan2  13740  grpnpncan  13741  grpnnncan2  13743  imasgrp2  13760  imasgrp  13761  mulgnndir  13801  mulgnn0dir  13802  mulgnnass  13807  mulgnn0ass  13808  mulgass  13809  issubg2m  13839  qusgrp  13882  kerf1ghm  13924  cmn32  13954  cmn12  13956  abladdsub  13965  ablsubsub23  13975  rngass  14016  imasrng  14033  srgdilem  14046  srgass  14048  ringdilem  14089  ringass  14093  ringrng  14113  imasring  14141  opprrng  14154  opprring  14156  mulgass3  14162  unitgrp  14194  dvrass  14217  dvrdir  14221  subrgunit  14317  issubrg2  14319  aprap  14365  lss1  14441  lsssn0  14449  islss3  14458  sralmod  14529  restopnb  14975  icnpimaex  15005  cnptopresti  15032  psmettri  15124  isxmet2d  15142  xmettri  15166  metrtri  15171  xmetres2  15173  bldisj  15195  blss2ps  15200  blss2  15201  xmstri2  15264  mstri2  15265  xmstri  15266  mstri  15267  xmstri3  15268  mstri3  15269  msrtri  15270  comet  15293  bdbl  15297  xmetxp  15301  dvconst  15488  dvconstre  15490  dvconstss  15492  sgmmul  15793  pw1ndom3  16693