Theorem simpr2 1035

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

Assertion

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

Proof of Theorem simpr2

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

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:  simplr2  1071  simprr2  1077  simp1r2  1125  simp2r2  1131  simp3r2  1137  3anandis  1388  isopolem  6028  tfrlemibacc  6597  tfrlemibfn  6599  tfr1onlembacc  6613  tfr1onlembfn  6615  tfrcllembacc  6626  tfrcllembfn  6628  prltlu  7854  prdisj  7859  prmuloc2  7934  ltntri  8454  eluzuzle  9932  xlesubadd  10287  elioc2  10340  elico2  10341  elicc2  10342  fseq1p1m1  10503  fz0fzelfz0  10536  seq3f1olemp  10954  bcval5  11203  hashdifpr  11263  hashtpgim  11299  swrdsbslen  11440  ccatswrd  11444  swrdswrdlem  11478  summodclem2  12151  isumss2  12162  tanaddap  12508  dvds2ln  12593  divalglemeunn  12690  divalglemex  12691  divalglemeuneg  12692  isstructr  13369  f1ovscpbl  13635  mndissubm  13784  grpsubrcan  13888  grpsubadd  13895  grpaddsubass  13897  grpsubsub4  13900  grppnpcan2  13901  grpnpncan  13902  mulgnndir  13956  mulgnn0dir  13957  mulgdir  13959  mulgnnass  13962  mulgnn0ass  13963  mulgass  13964  mulgsubdir  13967  issubg2m  13994  eqgval  14028  qusgrp  14037  cmn32  14109  cmn12  14111  abladdsub  14121  ablsubsub23  14131  prdssgrpd  14193  prdsmndd  14196  rngass  14240  srgdilem  14275  srgass  14277  ringdilem  14318  ringass  14322  opprrng  14384  opprring  14386  mulgass3  14393  unitgrp  14425  dvrass  14448  dvrdir  14452  subrgunit  14549  issubrg2  14551  aprap  14600  lsssn0  14709  islss3  14718  sralmod  14789  restopnb  15284  icnpimaex  15314  cnptopresti  15341  psmettri  15433  isxmet2d  15451  xmettri  15475  metrtri  15480  xmetres2  15482  bldisj  15504  blss2ps  15509  blss2  15510  xmstri2  15573  mstri2  15574  xmstri  15575  mstri  15576  xmstri3  15577  mstri3  15578  msrtri  15579  comet  15602  bdbl  15606  xmetxp  15610  dvconst  15797  dvconstre  15799  dvconstss  15801  sgmmul  16116  gausslemma2dlem1a  16189  pw1ndom3  17032