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  6031  suppfnss  6501  tfrlemibacc  6602  tfrlemibxssdm  6603  tfrlemibfn  6604  tfr1onlembacc  6618  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfrcllembacc  6631  tfrcllembxssdm  6632  tfrcllembfn  6633  elfir  7312  prloc  7864  prmuloc2  7940  ltntri  8461  eluzuzle  9945  xlesubadd  10301  elioc2  10354  elico2  10355  elicc2  10356  fseq1p1m1  10517  seq3f1olemp  10972  seq3f1oleml  10973  bcval5  11222  hashdifpr  11282  hashtpgim  11318  ccatswrd  11463  pfxccat3a  11531  isumss2  12184  tanaddap  12530  dvds2ln  12615  divalglemeunn  12712  divalglemex  12713  divalglemeuneg  12714  f1ovscpbl  13691  imasmnd2  13817  imasmnd  13818  grpsubadd  13951  grpaddsubass  13953  grpsubsub4  13956  grppnpcan2  13957  grpnpncan  13958  grpnnncan2  13960  imasgrp2  13971  imasgrp  13972  mulgnndir  14012  mulgnn0dir  14013  mulgnnass  14018  mulgnn0ass  14019  mulgass  14020  issubg2m  14050  qusgrp  14093  kerf1ghm  14135  cmn32  14196  cmn12  14198  abladdsub  14208  ablsubsub23  14218  prdssgrpd  14297  prdsmndd  14300  rngass  14344  imasrng  14361  srgdilem  14379  srgass  14381  ringdilem  14422  ringass  14426  ringrng  14447  imasring  14477  opprrng  14490  opprring  14492  mulgass3  14499  unitgrp  14531  dvrass  14554  dvrdir  14558  subrgunit  14655  issubrg2  14657  aprap  14706  lss1  14807  lsssn0  14815  islss3  14824  sralmod  14895  psrringfi  15213  mplsubgfilemcl  15232  mplsubgfileminv  15233  restopnb  15424  icnpimaex  15454  cnptopresti  15481  psmettri  15573  isxmet2d  15591  xmettri  15615  metrtri  15620  xmetres2  15622  bldisj  15644  blss2ps  15649  blss2  15650  xmstri2  15713  mstri2  15714  xmstri  15715  mstri  15716  xmstri3  15717  mstri3  15718  msrtri  15719  comet  15742  bdbl  15746  xmetxp  15750  dvconst  15937  dvconstre  15939  dvconstss  15941  sgmmul  16307  pw1ndom3  17242