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 )

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

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 1011

This theorem is referenced by:  simplr3  1072  simprr3  1078  simp1r3  1126  simp2r3  1132  simp3r3  1138  3anandis  1388  isopolem  6018  suppfnss  6487  tfrlemibacc  6587  tfrlemibxssdm  6588  tfrlemibfn  6589  tfr1onlembacc  6603  tfr1onlembxssdm  6604  tfr1onlembfn  6605  tfrcllembacc  6616  tfrcllembxssdm  6617  tfrcllembfn  6618  elfir  7297  prloc  7848  prmuloc2  7924  ltntri  8444  eluzuzle  9909  xlesubadd  10264  elioc2  10317  elico2  10318  elicc2  10319  fseq1p1m1  10479  seq3f1olemp  10930  seq3f1oleml  10931  bcval5  11179  hashdifpr  11239  hashtpgim  11275  ccatswrd  11420  pfxccat3a  11488  isumss2  12138  tanaddap  12484  dvds2ln  12569  divalglemeunn  12666  divalglemex  12667  divalglemeuneg  12668  f1ovscpbl  13610  imasmnd2  13736  imasmnd  13737  grpsubadd  13870  grpaddsubass  13872  grpsubsub4  13875  grppnpcan2  13876  grpnpncan  13877  grpnnncan2  13879  imasgrp2  13890  imasgrp  13891  mulgnndir  13931  mulgnn0dir  13932  mulgnnass  13937  mulgnn0ass  13938  mulgass  13939  issubg2m  13969  qusgrp  14012  kerf1ghm  14054  cmn32  14084  cmn12  14086  abladdsub  14096  ablsubsub23  14106  prdssgrpd  14168  prdsmndd  14171  rngass  14213  imasrng  14230  srgdilem  14247  srgass  14249  ringdilem  14290  ringass  14294  ringrng  14314  imasring  14342  opprrng  14355  opprring  14357  mulgass3  14364  unitgrp  14396  dvrass  14419  dvrdir  14423  subrgunit  14520  issubrg2  14522  aprap  14571  lss1  14671  lsssn0  14679  islss3  14688  sralmod  14759  restopnb  15205  icnpimaex  15235  cnptopresti  15262  psmettri  15354  isxmet2d  15372  xmettri  15396  metrtri  15401  xmetres2  15403  bldisj  15425  blss2ps  15430  blss2  15431  xmstri2  15494  mstri2  15495  xmstri  15496  mstri  15497  xmstri3  15498  mstri3  15499  msrtri  15500  comet  15523  bdbl  15527  xmetxp  15531  dvconst  15718  dvconstre  15720  dvconstss  15722  sgmmul  16024  pw1ndom3  16934