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  6001  suppfnss  6470  tfrlemibacc  6570  tfrlemibxssdm  6571  tfrlemibfn  6572  tfr1onlembacc  6586  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfrcllembacc  6599  tfrcllembxssdm  6600  tfrcllembfn  6601  elfir  7273  prloc  7822  prmuloc2  7898  ltntri  8417  eluzuzle  9880  xlesubadd  10235  elioc2  10288  elico2  10289  elicc2  10290  fseq1p1m1  10450  seq3f1olemp  10901  seq3f1oleml  10902  bcval5  11150  hashdifpr  11210  hashtpgim  11242  ccatswrd  11387  pfxccat3a  11455  isumss2  12104  tanaddap  12450  dvds2ln  12535  divalglemeunn  12632  divalglemex  12633  divalglemeuneg  12634  f1ovscpbl  13576  imasmnd2  13707  imasmnd  13708  grpsubadd  13843  grpaddsubass  13845  grpsubsub4  13848  grppnpcan2  13849  grpnpncan  13850  grpnnncan2  13852  imasgrp2  13863  imasgrp  13864  mulgnndir  13904  mulgnn0dir  13905  mulgnnass  13910  mulgnn0ass  13911  mulgass  13912  issubg2m  13942  qusgrp  13985  kerf1ghm  14027  cmn32  14057  cmn12  14059  abladdsub  14068  ablsubsub23  14078  prdssgrpd  14133  prdsmndd  14136  rngass  14178  imasrng  14195  srgdilem  14212  srgass  14214  ringdilem  14255  ringass  14259  ringrng  14279  imasring  14307  opprrng  14320  opprring  14322  mulgass3  14329  unitgrp  14361  dvrass  14384  dvrdir  14388  subrgunit  14485  issubrg2  14487  aprap  14536  lss1  14636  lsssn0  14644  islss3  14653  sralmod  14724  restopnb  15172  icnpimaex  15202  cnptopresti  15229  psmettri  15321  isxmet2d  15339  xmettri  15363  metrtri  15368  xmetres2  15370  bldisj  15392  blss2ps  15397  blss2  15398  xmstri2  15461  mstri2  15462  xmstri  15463  mstri  15464  xmstri3  15465  mstri3  15466  msrtri  15467  comet  15490  bdbl  15494  xmetxp  15498  dvconst  15685  dvconstre  15687  dvconstss  15689  sgmmul  15990  pw1ndom3  16890