Theorem simpr3 1029

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

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

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 1004

This theorem is referenced by:  simplr3  1065  simprr3  1071  simp1r3  1119  simp2r3  1125  simp3r3  1131  3anandis  1381  isopolem  5958  tfrlemibacc  6487  tfrlemibxssdm  6488  tfrlemibfn  6489  tfr1onlembacc  6503  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfrcllembacc  6516  tfrcllembxssdm  6517  tfrcllembfn  6518  elfir  7163  prloc  7701  prmuloc2  7777  ltntri  8297  eluzuzle  9754  xlesubadd  10108  elioc2  10161  elico2  10162  elicc2  10163  fseq1p1m1  10319  seq3f1olemp  10767  seq3f1oleml  10768  bcval5  11015  hashdifpr  11074  ccatswrd  11241  pfxccat3a  11309  isumss2  11944  tanaddap  12290  dvds2ln  12375  divalglemeunn  12472  divalglemex  12473  divalglemeuneg  12474  f1ovscpbl  13385  prdssgrpd  13488  prdsmndd  13521  imasmnd2  13525  imasmnd  13526  grpsubadd  13661  grpaddsubass  13663  grpsubsub4  13666  grppnpcan2  13667  grpnpncan  13668  grpnnncan2  13670  imasgrp2  13687  imasgrp  13688  mulgnndir  13728  mulgnn0dir  13729  mulgnnass  13734  mulgnn0ass  13735  mulgass  13736  issubg2m  13766  qusgrp  13809  kerf1ghm  13851  cmn32  13881  cmn12  13883  abladdsub  13892  ablsubsub23  13902  rngass  13942  imasrng  13959  srgdilem  13972  srgass  13974  ringdilem  14015  ringass  14019  ringrng  14039  imasring  14067  opprrng  14080  opprring  14082  mulgass3  14088  unitgrp  14120  dvrass  14143  dvrdir  14147  subrgunit  14243  issubrg2  14245  aprap  14290  lss1  14366  lsssn0  14374  islss3  14383  sralmod  14454  restopnb  14895  icnpimaex  14925  cnptopresti  14952  psmettri  15044  isxmet2d  15062  xmettri  15086  metrtri  15091  xmetres2  15093  bldisj  15115  blss2ps  15120  blss2  15121  xmstri2  15184  mstri2  15185  xmstri  15186  mstri  15187  xmstri3  15188  mstri3  15189  msrtri  15190  comet  15213  bdbl  15217  xmetxp  15221  dvconst  15408  dvconstre  15410  dvconstss  15412  sgmmul  15710  pw1ndom3  16525