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  6031  suppfnss  6501  tfrlemibacc  6601  tfrlemibxssdm  6602  tfrlemibfn  6603  tfr1onlembacc  6617  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfrcllembacc  6630  tfrcllembxssdm  6631  tfrcllembfn  6632  elfir  7312  prloc  7864  prmuloc2  7940  ltntri  8461  eluzuzle  9946  xlesubadd  10302  elioc2  10355  elico2  10356  elicc2  10357  fseq1p1m1  10518  seq3f1olemp  10973  seq3f1oleml  10974  bcval5  11223  hashdifpr  11283  hashtpgim  11319  ccatswrd  11464  pfxccat3a  11532  isumss2  12185  tanaddap  12531  dvds2ln  12616  divalglemeunn  12713  divalglemex  12714  divalglemeuneg  12715  f1ovscpbl  13692  imasmnd2  13818  imasmnd  13819  grpsubadd  13952  grpaddsubass  13954  grpsubsub4  13957  grppnpcan2  13958  grpnpncan  13959  grpnnncan2  13961  imasgrp2  13972  imasgrp  13973  mulgnndir  14013  mulgnn0dir  14014  mulgnnass  14019  mulgnn0ass  14020  mulgass  14021  issubg2m  14051  qusgrp  14094  kerf1ghm  14136  cmn32  14197  cmn12  14199  abladdsub  14209  ablsubsub23  14219  prdssgrpd  14298  prdsmndd  14301  rngass  14345  imasrng  14362  srgdilem  14380  srgass  14382  ringdilem  14423  ringass  14427  ringrng  14448  imasring  14478  opprrng  14491  opprring  14493  mulgass3  14500  unitgrp  14532  dvrass  14555  dvrdir  14559  subrgunit  14656  issubrg2  14658  aprap  14707  lss1  14808  lsssn0  14816  islss3  14825  sralmod  14896  psrringfi  15204  restopnb  15407  icnpimaex  15437  cnptopresti  15464  psmettri  15556  isxmet2d  15574  xmettri  15598  metrtri  15603  xmetres2  15605  bldisj  15627  blss2ps  15632  blss2  15633  xmstri2  15696  mstri2  15697  xmstri  15698  mstri  15699  xmstri3  15700  mstri3  15701  msrtri  15702  comet  15725  bdbl  15729  xmetxp  15733  dvconst  15920  dvconstre  15922  dvconstss  15924  sgmmul  16290  pw1ndom3  17225