Theorem simpr2 1028

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

Assertion

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

Proof of Theorem simpr2

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

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:  simplr2  1064  simprr2  1070  simp1r2  1118  simp2r2  1124  simp3r2  1130  3anandis  1381  isopolem  5952  tfrlemibacc  6478  tfrlemibfn  6480  tfr1onlembacc  6494  tfr1onlembfn  6496  tfrcllembacc  6507  tfrcllembfn  6509  prltlu  7682  prdisj  7687  prmuloc2  7762  ltntri  8282  eluzuzle  9738  xlesubadd  10087  elioc2  10140  elico2  10141  elicc2  10142  fseq1p1m1  10298  fz0fzelfz0  10331  seq3f1olemp  10745  bcval5  10993  hashdifpr  11050  swrdsbslen  11206  ccatswrd  11210  swrdswrdlem  11244  summodclem2  11901  isumss2  11912  tanaddap  12258  dvds2ln  12343  divalglemeunn  12440  divalglemex  12441  divalglemeuneg  12442  isstructr  13055  f1ovscpbl  13353  prdssgrpd  13456  prdsmndd  13489  mndissubm  13516  grpsubrcan  13622  grpsubadd  13629  grpaddsubass  13631  grpsubsub4  13634  grppnpcan2  13635  grpnpncan  13636  mulgnndir  13696  mulgnn0dir  13697  mulgdir  13699  mulgnnass  13702  mulgnn0ass  13703  mulgass  13704  mulgsubdir  13707  issubg2m  13734  eqgval  13768  qusgrp  13777  cmn32  13849  cmn12  13851  abladdsub  13860  ablsubsub23  13870  rngass  13910  srgdilem  13940  srgass  13942  ringdilem  13983  ringass  13987  opprrng  14048  opprring  14050  mulgass3  14056  unitgrp  14088  dvrass  14111  dvrdir  14115  subrgunit  14211  issubrg2  14213  aprap  14258  lsssn0  14342  islss3  14351  sralmod  14422  restopnb  14863  icnpimaex  14893  cnptopresti  14920  psmettri  15012  isxmet2d  15030  xmettri  15054  metrtri  15059  xmetres2  15061  bldisj  15083  blss2ps  15088  blss2  15089  xmstri2  15152  mstri2  15153  xmstri  15154  mstri  15155  xmstri3  15156  mstri3  15157  msrtri  15158  comet  15181  bdbl  15185  xmetxp  15189  dvconst  15376  dvconstre  15378  dvconstss  15380  sgmmul  15678  gausslemma2dlem1a  15745  pw1ndom3  16383