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  7573  prdisj  7578  prmuloc2  7653  ltntri  8173  eluzuzle  9628  xlesubadd  9977  elioc2  10030  elico2  10031  elicc2  10032  fseq1p1m1  10188  fz0fzelfz0  10221  seq3f1olemp  10626  bcval5  10874  hashdifpr  10931  summodclem2  11566  isumss2  11577  tanaddap  11923  dvds2ln  12008  divalglemeunn  12105  divalglemex  12106  divalglemeuneg  12107  isstructr  12720  f1ovscpbl  13016  prdssgrpd  13119  prdsmndd  13152  mndissubm  13179  grpsubrcan  13285  grpsubadd  13292  grpaddsubass  13294  grpsubsub4  13297  grppnpcan2  13298  grpnpncan  13299  mulgnndir  13359  mulgnn0dir  13360  mulgdir  13362  mulgnnass  13365  mulgnn0ass  13366  mulgass  13367  mulgsubdir  13370  issubg2m  13397  eqgval  13431  qusgrp  13440  cmn32  13512  cmn12  13514  abladdsub  13523  ablsubsub23  13533  rngass  13573  srgdilem  13603  srgass  13605  ringdilem  13646  ringass  13650  opprrng  13711  opprring  13713  mulgass3  13719  unitgrp  13750  dvrass  13773  dvrdir  13777  subrgunit  13873  issubrg2  13875  aprap  13920  lsssn0  14004  islss3  14013  sralmod  14084  restopnb  14503  icnpimaex  14533  cnptopresti  14560  psmettri  14652  isxmet2d  14670  xmettri  14694  metrtri  14699  xmetres2  14701  bldisj  14723  blss2ps  14728  blss2  14729  xmstri2  14792  mstri2  14793  xmstri  14794  mstri  14795  xmstri3  14796  mstri3  14797  msrtri  14798  comet  14821  bdbl  14825  xmetxp  14829  dvconst  15016  dvconstre  15018  dvconstss  15020  sgmmul  15318  gausslemma2dlem1a  15385