Theorem simpr2 1007

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

Assertion

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

Proof of Theorem simpr2

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

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

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 983

This theorem is referenced by:  simplr2  1043  simprr2  1049  simp1r2  1097  simp2r2  1103  simp3r2  1109  3anandis  1360  isopolem  5898  tfrlemibacc  6419  tfrlemibfn  6421  tfr1onlembacc  6435  tfr1onlembfn  6437  tfrcllembacc  6448  tfrcllembfn  6450  prltlu  7607  prdisj  7612  prmuloc2  7687  ltntri  8207  eluzuzle  9663  xlesubadd  10012  elioc2  10065  elico2  10066  elicc2  10067  fseq1p1m1  10223  fz0fzelfz0  10256  seq3f1olemp  10667  bcval5  10915  hashdifpr  10972  swrdsbslen  11127  ccatswrd  11131  swrdswrdlem  11163  summodclem2  11737  isumss2  11748  tanaddap  12094  dvds2ln  12179  divalglemeunn  12276  divalglemex  12277  divalglemeuneg  12278  isstructr  12891  f1ovscpbl  13188  prdssgrpd  13291  prdsmndd  13324  mndissubm  13351  grpsubrcan  13457  grpsubadd  13464  grpaddsubass  13466  grpsubsub4  13469  grppnpcan2  13470  grpnpncan  13471  mulgnndir  13531  mulgnn0dir  13532  mulgdir  13534  mulgnnass  13537  mulgnn0ass  13538  mulgass  13539  mulgsubdir  13542  issubg2m  13569  eqgval  13603  qusgrp  13612  cmn32  13684  cmn12  13686  abladdsub  13695  ablsubsub23  13705  rngass  13745  srgdilem  13775  srgass  13777  ringdilem  13818  ringass  13822  opprrng  13883  opprring  13885  mulgass3  13891  unitgrp  13922  dvrass  13945  dvrdir  13949  subrgunit  14045  issubrg2  14047  aprap  14092  lsssn0  14176  islss3  14185  sralmod  14256  restopnb  14697  icnpimaex  14727  cnptopresti  14754  psmettri  14846  isxmet2d  14864  xmettri  14888  metrtri  14893  xmetres2  14895  bldisj  14917  blss2ps  14922  blss2  14923  xmstri2  14986  mstri2  14987  xmstri  14988  mstri  14989  xmstri3  14990  mstri3  14991  msrtri  14992  comet  15015  bdbl  15019  xmetxp  15023  dvconst  15210  dvconstre  15212  dvconstss  15214  sgmmul  15512  gausslemma2dlem1a  15579