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  5945  tfrlemibacc  6470  tfrlemibxssdm  6471  tfrlemibfn  6472  tfr1onlembacc  6486  tfr1onlembxssdm  6487  tfr1onlembfn  6488  tfrcllembacc  6499  tfrcllembxssdm  6500  tfrcllembfn  6501  elfir  7136  prloc  7674  prmuloc2  7750  ltntri  8270  eluzuzle  9726  xlesubadd  10075  elioc2  10128  elico2  10129  elicc2  10130  fseq1p1m1  10286  seq3f1olemp  10732  seq3f1oleml  10733  bcval5  10980  hashdifpr  11037  ccatswrd  11197  pfxccat3a  11265  isumss2  11899  tanaddap  12245  dvds2ln  12330  divalglemeunn  12427  divalglemex  12428  divalglemeuneg  12429  f1ovscpbl  13340  prdssgrpd  13443  prdsmndd  13476  imasmnd2  13480  imasmnd  13481  grpsubadd  13616  grpaddsubass  13618  grpsubsub4  13621  grppnpcan2  13622  grpnpncan  13623  grpnnncan2  13625  imasgrp2  13642  imasgrp  13643  mulgnndir  13683  mulgnn0dir  13684  mulgnnass  13689  mulgnn0ass  13690  mulgass  13691  issubg2m  13721  qusgrp  13764  kerf1ghm  13806  cmn32  13836  cmn12  13838  abladdsub  13847  ablsubsub23  13857  rngass  13897  imasrng  13914  srgdilem  13927  srgass  13929  ringdilem  13970  ringass  13974  ringrng  13994  imasring  14022  opprrng  14035  opprring  14037  mulgass3  14043  unitgrp  14074  dvrass  14097  dvrdir  14101  subrgunit  14197  issubrg2  14199  aprap  14244  lss1  14320  lsssn0  14328  islss3  14337  sralmod  14408  restopnb  14849  icnpimaex  14879  cnptopresti  14906  psmettri  14998  isxmet2d  15016  xmettri  15040  metrtri  15045  xmetres2  15047  bldisj  15069  blss2ps  15074  blss2  15075  xmstri2  15138  mstri2  15139  xmstri  15140  mstri  15141  xmstri3  15142  mstri3  15143  msrtri  15144  comet  15167  bdbl  15171  xmetxp  15175  dvconst  15362  dvconstre  15364  dvconstss  15366  sgmmul  15664