Theorem simpr3 1036

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

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:  simplr3  1072  simprr3  1078  simp1r3  1126  simp2r3  1132  simp3r3  1138  3anandis  1388  isopolem  6028  suppfnss  6497  tfrlemibacc  6597  tfrlemibxssdm  6598  tfrlemibfn  6599  tfr1onlembacc  6613  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfrcllembacc  6626  tfrcllembxssdm  6627  tfrcllembfn  6628  elfir  7307  prloc  7858  prmuloc2  7934  ltntri  8454  eluzuzle  9930  xlesubadd  10285  elioc2  10338  elico2  10339  elicc2  10340  fseq1p1m1  10501  seq3f1olemp  10952  seq3f1oleml  10953  bcval5  11201  hashdifpr  11261  hashtpgim  11297  ccatswrd  11442  pfxccat3a  11510  isumss2  12160  tanaddap  12506  dvds2ln  12591  divalglemeunn  12688  divalglemex  12689  divalglemeuneg  12690  f1ovscpbl  13633  imasmnd2  13759  imasmnd  13760  grpsubadd  13893  grpaddsubass  13895  grpsubsub4  13898  grppnpcan2  13899  grpnpncan  13900  grpnnncan2  13902  imasgrp2  13913  imasgrp  13914  mulgnndir  13954  mulgnn0dir  13955  mulgnnass  13960  mulgnn0ass  13961  mulgass  13962  issubg2m  13992  qusgrp  14035  kerf1ghm  14077  cmn32  14107  cmn12  14109  abladdsub  14119  ablsubsub23  14129  prdssgrpd  14191  prdsmndd  14194  rngass  14238  imasrng  14255  srgdilem  14273  srgass  14275  ringdilem  14316  ringass  14320  ringrng  14341  imasring  14369  opprrng  14382  opprring  14384  mulgass3  14391  unitgrp  14423  dvrass  14446  dvrdir  14450  subrgunit  14547  issubrg2  14549  aprap  14598  lss1  14699  lsssn0  14707  islss3  14716  sralmod  14787  restopnb  15282  icnpimaex  15312  cnptopresti  15339  psmettri  15431  isxmet2d  15449  xmettri  15473  metrtri  15478  xmetres2  15480  bldisj  15502  blss2ps  15507  blss2  15508  xmstri2  15571  mstri2  15572  xmstri  15573  mstri  15574  xmstri3  15575  mstri3  15576  msrtri  15577  comet  15600  bdbl  15604  xmetxp  15608  dvconst  15795  dvconstre  15797  dvconstss  15799  sgmmul  16110  pw1ndom3  17020