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  5995  suppfnss  6457  tfrlemibacc  6557  tfrlemibxssdm  6558  tfrlemibfn  6559  tfr1onlembacc  6573  tfr1onlembxssdm  6574  tfr1onlembfn  6575  tfrcllembacc  6586  tfrcllembxssdm  6587  tfrcllembfn  6588  elfir  7260  prloc  7806  prmuloc2  7882  ltntri  8401  eluzuzle  9862  xlesubadd  10216  elioc2  10269  elico2  10270  elicc2  10271  fseq1p1m1  10428  seq3f1olemp  10877  seq3f1oleml  10878  bcval5  11125  hashdifpr  11185  hashtpgim  11215  ccatswrd  11360  pfxccat3a  11428  isumss2  12077  tanaddap  12423  dvds2ln  12508  divalglemeunn  12605  divalglemex  12606  divalglemeuneg  12607  f1ovscpbl  13523  prdssgrpd  13626  prdsmndd  13659  imasmnd2  13663  imasmnd  13664  grpsubadd  13799  grpaddsubass  13801  grpsubsub4  13804  grppnpcan2  13805  grpnpncan  13806  grpnnncan2  13808  imasgrp2  13825  imasgrp  13826  mulgnndir  13866  mulgnn0dir  13867  mulgnnass  13872  mulgnn0ass  13873  mulgass  13874  issubg2m  13904  qusgrp  13947  kerf1ghm  13989  cmn32  14019  cmn12  14021  abladdsub  14030  ablsubsub23  14040  rngass  14081  imasrng  14098  srgdilem  14111  srgass  14113  ringdilem  14154  ringass  14158  ringrng  14178  imasring  14206  opprrng  14219  opprring  14221  mulgass3  14227  unitgrp  14259  dvrass  14282  dvrdir  14286  subrgunit  14382  issubrg2  14384  aprap  14430  lss1  14508  lsssn0  14516  islss3  14525  sralmod  14596  restopnb  15044  icnpimaex  15074  cnptopresti  15101  psmettri  15193  isxmet2d  15211  xmettri  15235  metrtri  15240  xmetres2  15242  bldisj  15264  blss2ps  15269  blss2  15270  xmstri2  15333  mstri2  15334  xmstri  15335  mstri  15336  xmstri3  15337  mstri3  15338  msrtri  15339  comet  15362  bdbl  15366  xmetxp  15370  dvconst  15557  dvconstre  15559  dvconstss  15561  sgmmul  15862  pw1ndom3  16762