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  7859  prmuloc2  7935  ltntri  8456  eluzuzle  9940  xlesubadd  10296  elioc2  10349  elico2  10350  elicc2  10351  fseq1p1m1  10512  seq3f1olemp  10967  seq3f1oleml  10968  bcval5  11217  hashdifpr  11277  hashtpgim  11313  ccatswrd  11458  pfxccat3a  11526  isumss2  12179  tanaddap  12525  dvds2ln  12610  divalglemeunn  12707  divalglemex  12708  divalglemeuneg  12709  f1ovscpbl  13686  imasmnd2  13812  imasmnd  13813  grpsubadd  13946  grpaddsubass  13948  grpsubsub4  13951  grppnpcan2  13952  grpnpncan  13953  grpnnncan2  13955  imasgrp2  13966  imasgrp  13967  mulgnndir  14007  mulgnn0dir  14008  mulgnnass  14013  mulgnn0ass  14014  mulgass  14015  issubg2m  14045  qusgrp  14088  kerf1ghm  14130  cmn32  14191  cmn12  14193  abladdsub  14203  ablsubsub23  14213  prdssgrpd  14275  prdsmndd  14278  rngass  14322  imasrng  14339  srgdilem  14357  srgass  14359  ringdilem  14400  ringass  14404  ringrng  14425  imasring  14453  opprrng  14466  opprring  14468  mulgass3  14475  unitgrp  14507  dvrass  14530  dvrdir  14534  subrgunit  14631  issubrg2  14633  aprap  14682  lss1  14783  lsssn0  14791  islss3  14800  sralmod  14871  restopnb  15373  icnpimaex  15403  cnptopresti  15430  psmettri  15522  isxmet2d  15540  xmettri  15564  metrtri  15569  xmetres2  15571  bldisj  15593  blss2ps  15598  blss2  15599  xmstri2  15662  mstri2  15663  xmstri  15664  mstri  15665  xmstri3  15666  mstri3  15667  msrtri  15668  comet  15691  bdbl  15695  xmetxp  15699  dvconst  15886  dvconstre  15888  dvconstss  15890  sgmmul  16251  pw1ndom3  17186