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  5955  tfrlemibacc  6483  tfrlemibfn  6485  tfr1onlembacc  6499  tfr1onlembfn  6501  tfrcllembacc  6512  tfrcllembfn  6514  prltlu  7690  prdisj  7695  prmuloc2  7770  ltntri  8290  eluzuzle  9747  xlesubadd  10096  elioc2  10149  elico2  10150  elicc2  10151  fseq1p1m1  10307  fz0fzelfz0  10340  seq3f1olemp  10754  bcval5  11002  hashdifpr  11060  swrdsbslen  11219  ccatswrd  11223  swrdswrdlem  11257  summodclem2  11914  isumss2  11925  tanaddap  12271  dvds2ln  12356  divalglemeunn  12453  divalglemex  12454  divalglemeuneg  12455  isstructr  13068  f1ovscpbl  13366  prdssgrpd  13469  prdsmndd  13502  mndissubm  13529  grpsubrcan  13635  grpsubadd  13642  grpaddsubass  13644  grpsubsub4  13647  grppnpcan2  13648  grpnpncan  13649  mulgnndir  13709  mulgnn0dir  13710  mulgdir  13712  mulgnnass  13715  mulgnn0ass  13716  mulgass  13717  mulgsubdir  13720  issubg2m  13747  eqgval  13781  qusgrp  13790  cmn32  13862  cmn12  13864  abladdsub  13873  ablsubsub23  13883  rngass  13923  srgdilem  13953  srgass  13955  ringdilem  13996  ringass  14000  opprrng  14061  opprring  14063  mulgass3  14069  unitgrp  14101  dvrass  14124  dvrdir  14128  subrgunit  14224  issubrg2  14226  aprap  14271  lsssn0  14355  islss3  14364  sralmod  14435  restopnb  14876  icnpimaex  14906  cnptopresti  14933  psmettri  15025  isxmet2d  15043  xmettri  15067  metrtri  15072  xmetres2  15074  bldisj  15096  blss2ps  15101  blss2  15102  xmstri2  15165  mstri2  15166  xmstri  15167  mstri  15168  xmstri3  15169  mstri3  15170  msrtri  15171  comet  15194  bdbl  15198  xmetxp  15202  dvconst  15389  dvconstre  15391  dvconstss  15393  sgmmul  15691  gausslemma2dlem1a  15758  pw1ndom3  16467