Theorem simpr3 1008

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

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

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 983

This theorem is referenced by:  simplr3  1044  simprr3  1050  simp1r3  1098  simp2r3  1104  simp3r3  1110  3anandis  1360  isopolem  5891  tfrlemibacc  6412  tfrlemibxssdm  6413  tfrlemibfn  6414  tfr1onlembacc  6428  tfr1onlembxssdm  6429  tfr1onlembfn  6430  tfrcllembacc  6441  tfrcllembxssdm  6442  tfrcllembfn  6443  elfir  7075  prloc  7604  prmuloc2  7680  ltntri  8200  eluzuzle  9656  xlesubadd  10005  elioc2  10058  elico2  10059  elicc2  10060  fseq1p1m1  10216  seq3f1olemp  10660  seq3f1oleml  10661  bcval5  10908  hashdifpr  10965  ccatswrd  11123  isumss2  11704  tanaddap  12050  dvds2ln  12135  divalglemeunn  12232  divalglemex  12233  divalglemeuneg  12234  f1ovscpbl  13144  prdssgrpd  13247  prdsmndd  13280  imasmnd2  13284  imasmnd  13285  grpsubadd  13420  grpaddsubass  13422  grpsubsub4  13425  grppnpcan2  13426  grpnpncan  13427  grpnnncan2  13429  imasgrp2  13446  imasgrp  13447  mulgnndir  13487  mulgnn0dir  13488  mulgnnass  13493  mulgnn0ass  13494  mulgass  13495  issubg2m  13525  qusgrp  13568  kerf1ghm  13610  cmn32  13640  cmn12  13642  abladdsub  13651  ablsubsub23  13661  rngass  13701  imasrng  13718  srgdilem  13731  srgass  13733  ringdilem  13774  ringass  13778  ringrng  13798  imasring  13826  opprrng  13839  opprring  13841  mulgass3  13847  unitgrp  13878  dvrass  13901  dvrdir  13905  subrgunit  14001  issubrg2  14003  aprap  14048  lss1  14124  lsssn0  14132  islss3  14141  sralmod  14212  restopnb  14653  icnpimaex  14683  cnptopresti  14710  psmettri  14802  isxmet2d  14820  xmettri  14844  metrtri  14849  xmetres2  14851  bldisj  14873  blss2ps  14878  blss2  14879  xmstri2  14942  mstri2  14943  xmstri  14944  mstri  14945  xmstri3  14946  mstri3  14947  msrtri  14948  comet  14971  bdbl  14975  xmetxp  14979  dvconst  15166  dvconstre  15168  dvconstss  15170  sgmmul  15468