Theorem simpr2 1006

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpr2	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒)

Proof of Theorem simpr2

Step	Hyp	Ref	Expression
1		simp2 1000	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜒)
2	1	adantl 277	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 980

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 982

This theorem is referenced by:  simplr2  1042  simprr2  1048  simp1r2  1096  simp2r2  1102  simp3r2  1108  3anandis  1358  isopolem  5872  tfrlemibacc  6393  tfrlemibfn  6395  tfr1onlembacc  6409  tfr1onlembfn  6411  tfrcllembacc  6422  tfrcllembfn  6424  prltlu  7571  prdisj  7576  prmuloc2  7651  ltntri  8171  eluzuzle  9626  xlesubadd  9975  elioc2  10028  elico2  10029  elicc2  10030  fseq1p1m1  10186  fz0fzelfz0  10219  seq3f1olemp  10624  bcval5  10872  hashdifpr  10929  summodclem2  11564  isumss2  11575  tanaddap  11921  dvds2ln  12006  divalglemeunn  12103  divalglemex  12104  divalglemeuneg  12105  isstructr  12718  f1ovscpbl  13014  prdssgrpd  13117  prdsmndd  13150  mndissubm  13177  grpsubrcan  13283  grpsubadd  13290  grpaddsubass  13292  grpsubsub4  13295  grppnpcan2  13296  grpnpncan  13297  mulgnndir  13357  mulgnn0dir  13358  mulgdir  13360  mulgnnass  13363  mulgnn0ass  13364  mulgass  13365  mulgsubdir  13368  issubg2m  13395  eqgval  13429  qusgrp  13438  cmn32  13510  cmn12  13512  abladdsub  13521  ablsubsub23  13531  rngass  13571  srgdilem  13601  srgass  13603  ringdilem  13644  ringass  13648  opprrng  13709  opprring  13711  mulgass3  13717  unitgrp  13748  dvrass  13771  dvrdir  13775  subrgunit  13871  issubrg2  13873  aprap  13918  lsssn0  14002  islss3  14011  sralmod  14082  restopnb  14501  icnpimaex  14531  cnptopresti  14558  psmettri  14650  isxmet2d  14668  xmettri  14692  metrtri  14697  xmetres2  14699  bldisj  14721  blss2ps  14726  blss2  14727  xmstri2  14790  mstri2  14791  xmstri  14792  mstri  14793  xmstri3  14794  mstri3  14795  msrtri  14796  comet  14819  bdbl  14823  xmetxp  14827  dvconst  15014  dvconstre  15016  dvconstss  15018  sgmmul  15316  gausslemma2dlem1a  15383