Theorem simpr3 1031

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

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

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 1006

This theorem is referenced by:  simplr3  1067  simprr3  1073  simp1r3  1121  simp2r3  1127  simp3r3  1133  3anandis  1383  isopolem  5962  tfrlemibacc  6491  tfrlemibxssdm  6492  tfrlemibfn  6493  tfr1onlembacc  6507  tfr1onlembxssdm  6508  tfr1onlembfn  6509  tfrcllembacc  6520  tfrcllembxssdm  6521  tfrcllembfn  6522  elfir  7171  prloc  7710  prmuloc2  7786  ltntri  8306  eluzuzle  9763  xlesubadd  10117  elioc2  10170  elico2  10171  elicc2  10172  fseq1p1m1  10328  seq3f1olemp  10776  seq3f1oleml  10777  bcval5  11024  hashdifpr  11083  ccatswrd  11250  pfxccat3a  11318  isumss2  11953  tanaddap  12299  dvds2ln  12384  divalglemeunn  12481  divalglemex  12482  divalglemeuneg  12483  f1ovscpbl  13394  prdssgrpd  13497  prdsmndd  13530  imasmnd2  13534  imasmnd  13535  grpsubadd  13670  grpaddsubass  13672  grpsubsub4  13675  grppnpcan2  13676  grpnpncan  13677  grpnnncan2  13679  imasgrp2  13696  imasgrp  13697  mulgnndir  13737  mulgnn0dir  13738  mulgnnass  13743  mulgnn0ass  13744  mulgass  13745  issubg2m  13775  qusgrp  13818  kerf1ghm  13860  cmn32  13890  cmn12  13892  abladdsub  13901  ablsubsub23  13911  rngass  13951  imasrng  13968  srgdilem  13981  srgass  13983  ringdilem  14024  ringass  14028  ringrng  14048  imasring  14076  opprrng  14089  opprring  14091  mulgass3  14097  unitgrp  14129  dvrass  14152  dvrdir  14156  subrgunit  14252  issubrg2  14254  aprap  14299  lss1  14375  lsssn0  14383  islss3  14392  sralmod  14463  restopnb  14904  icnpimaex  14934  cnptopresti  14961  psmettri  15053  isxmet2d  15071  xmettri  15095  metrtri  15100  xmetres2  15102  bldisj  15124  blss2ps  15129  blss2  15130  xmstri2  15193  mstri2  15194  xmstri  15195  mstri  15196  xmstri3  15197  mstri3  15198  msrtri  15199  comet  15222  bdbl  15226  xmetxp  15230  dvconst  15417  dvconstre  15419  dvconstss  15421  sgmmul  15719  pw1ndom3  16589