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  6028  suppfnss  6497  tfrlemibacc  6597  tfrlemibxssdm  6598  tfrlemibfn  6599  tfr1onlembacc  6613  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfrcllembacc  6626  tfrcllembxssdm  6627  tfrcllembfn  6628  elfir  7307  prloc  7858  prmuloc2  7934  ltntri  8455  eluzuzle  9939  xlesubadd  10295  elioc2  10348  elico2  10349  elicc2  10350  fseq1p1m1  10511  seq3f1olemp  10965  seq3f1oleml  10966  bcval5  11215  hashdifpr  11275  hashtpgim  11311  ccatswrd  11456  pfxccat3a  11524  isumss2  12176  tanaddap  12522  dvds2ln  12607  divalglemeunn  12704  divalglemex  12705  divalglemeuneg  12706  f1ovscpbl  13682  imasmnd2  13808  imasmnd  13809  grpsubadd  13942  grpaddsubass  13944  grpsubsub4  13947  grppnpcan2  13948  grpnpncan  13949  grpnnncan2  13951  imasgrp2  13962  imasgrp  13963  mulgnndir  14003  mulgnn0dir  14004  mulgnnass  14009  mulgnn0ass  14010  mulgass  14011  issubg2m  14041  qusgrp  14084  kerf1ghm  14126  cmn32  14156  cmn12  14158  abladdsub  14168  ablsubsub23  14178  prdssgrpd  14240  prdsmndd  14243  rngass  14287  imasrng  14304  srgdilem  14322  srgass  14324  ringdilem  14365  ringass  14369  ringrng  14390  imasring  14418  opprrng  14431  opprring  14433  mulgass3  14440  unitgrp  14472  dvrass  14495  dvrdir  14499  subrgunit  14596  issubrg2  14598  aprap  14647  lss1  14748  lsssn0  14756  islss3  14765  sralmod  14836  restopnb  15331  icnpimaex  15361  cnptopresti  15388  psmettri  15480  isxmet2d  15498  xmettri  15522  metrtri  15527  xmetres2  15529  bldisj  15551  blss2ps  15556  blss2  15557  xmstri2  15620  mstri2  15621  xmstri  15622  mstri  15623  xmstri3  15624  mstri3  15625  msrtri  15626  comet  15649  bdbl  15653  xmetxp  15657  dvconst  15844  dvconstre  15846  dvconstss  15848  sgmmul  16191  pw1ndom3  17118