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  11217  ccatswrd  11362  pfxccat3a  11430  isumss2  12079  tanaddap  12425  dvds2ln  12510  divalglemeunn  12607  divalglemex  12608  divalglemeuneg  12609  f1ovscpbl  13525  prdssgrpd  13628  prdsmndd  13661  imasmnd2  13665  imasmnd  13666  grpsubadd  13801  grpaddsubass  13803  grpsubsub4  13806  grppnpcan2  13807  grpnpncan  13808  grpnnncan2  13810  imasgrp2  13827  imasgrp  13828  mulgnndir  13868  mulgnn0dir  13869  mulgnnass  13874  mulgnn0ass  13875  mulgass  13876  issubg2m  13906  qusgrp  13949  kerf1ghm  13991  cmn32  14021  cmn12  14023  abladdsub  14032  ablsubsub23  14042  rngass  14083  imasrng  14100  srgdilem  14113  srgass  14115  ringdilem  14156  ringass  14160  ringrng  14180  imasring  14208  opprrng  14221  opprring  14223  mulgass3  14229  unitgrp  14261  dvrass  14284  dvrdir  14288  subrgunit  14384  issubrg2  14386  aprap  14432  lss1  14510  lsssn0  14518  islss3  14527  sralmod  14598  restopnb  15046  icnpimaex  15076  cnptopresti  15103  psmettri  15195  isxmet2d  15213  xmettri  15237  metrtri  15242  xmetres2  15244  bldisj  15266  blss2ps  15271  blss2  15272  xmstri2  15335  mstri2  15336  xmstri  15337  mstri  15338  xmstri3  15339  mstri3  15340  msrtri  15341  comet  15364  bdbl  15368  xmetxp  15372  dvconst  15559  dvconstre  15561  dvconstss  15563  sgmmul  15864  pw1ndom3  16764