Theorem simpr3 1008

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 981

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 983

This theorem is referenced by:  simplr3  1044  simprr3  1050  simp1r3  1098  simp2r3  1104  simp3r3  1110  3anandis  1360  isopolem  5909  tfrlemibacc  6430  tfrlemibxssdm  6431  tfrlemibfn  6432  tfr1onlembacc  6446  tfr1onlembxssdm  6447  tfr1onlembfn  6448  tfrcllembacc  6459  tfrcllembxssdm  6460  tfrcllembfn  6461  elfir  7096  prloc  7634  prmuloc2  7710  ltntri  8230  eluzuzle  9686  xlesubadd  10035  elioc2  10088  elico2  10089  elicc2  10090  fseq1p1m1  10246  seq3f1olemp  10692  seq3f1oleml  10693  bcval5  10940  hashdifpr  10997  ccatswrd  11156  isumss2  11789  tanaddap  12135  dvds2ln  12220  divalglemeunn  12317  divalglemex  12318  divalglemeuneg  12319  f1ovscpbl  13229  prdssgrpd  13332  prdsmndd  13365  imasmnd2  13369  imasmnd  13370  grpsubadd  13505  grpaddsubass  13507  grpsubsub4  13510  grppnpcan2  13511  grpnpncan  13512  grpnnncan2  13514  imasgrp2  13531  imasgrp  13532  mulgnndir  13572  mulgnn0dir  13573  mulgnnass  13578  mulgnn0ass  13579  mulgass  13580  issubg2m  13610  qusgrp  13653  kerf1ghm  13695  cmn32  13725  cmn12  13727  abladdsub  13736  ablsubsub23  13746  rngass  13786  imasrng  13803  srgdilem  13816  srgass  13818  ringdilem  13859  ringass  13863  ringrng  13883  imasring  13911  opprrng  13924  opprring  13926  mulgass3  13932  unitgrp  13963  dvrass  13986  dvrdir  13990  subrgunit  14086  issubrg2  14088  aprap  14133  lss1  14209  lsssn0  14217  islss3  14226  sralmod  14297  restopnb  14738  icnpimaex  14768  cnptopresti  14795  psmettri  14887  isxmet2d  14905  xmettri  14929  metrtri  14934  xmetres2  14936  bldisj  14958  blss2ps  14963  blss2  14964  xmstri2  15027  mstri2  15028  xmstri  15029  mstri  15030  xmstri3  15031  mstri3  15032  msrtri  15033  comet  15056  bdbl  15060  xmetxp  15064  dvconst  15251  dvconstre  15253  dvconstss  15255  sgmmul  15553