Theorem simpr2 1031

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

Assertion

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

Proof of Theorem simpr2

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

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

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 1007

This theorem is referenced by:  simplr2  1067  simprr2  1073  simp1r2  1121  simp2r2  1127  simp3r2  1133  3anandis  1384  isopolem  5997  tfrlemibacc  6559  tfrlemibfn  6561  tfr1onlembacc  6575  tfr1onlembfn  6577  tfrcllembacc  6588  tfrcllembfn  6590  prltlu  7807  prdisj  7812  prmuloc2  7887  ltntri  8406  eluzuzle  9868  xlesubadd  10222  elioc2  10275  elico2  10276  elicc2  10277  fseq1p1m1  10435  fz0fzelfz0  10468  seq3f1olemp  10884  bcval5  11133  hashdifpr  11193  hashtpgim  11225  swrdsbslen  11366  ccatswrd  11370  swrdswrdlem  11404  summodclem2  12076  isumss2  12087  tanaddap  12433  dvds2ln  12518  divalglemeunn  12615  divalglemex  12616  divalglemeuneg  12617  isstructr  13248  f1ovscpbl  13546  prdssgrpd  13649  prdsmndd  13682  mndissubm  13709  grpsubrcan  13815  grpsubadd  13822  grpaddsubass  13824  grpsubsub4  13827  grppnpcan2  13828  grpnpncan  13829  mulgnndir  13889  mulgnn0dir  13890  mulgdir  13892  mulgnnass  13895  mulgnn0ass  13896  mulgass  13897  mulgsubdir  13900  issubg2m  13927  eqgval  13961  qusgrp  13970  cmn32  14042  cmn12  14044  abladdsub  14053  ablsubsub23  14063  rngass  14104  srgdilem  14134  srgass  14136  ringdilem  14177  ringass  14181  opprrng  14242  opprring  14244  mulgass3  14251  unitgrp  14283  dvrass  14306  dvrdir  14310  subrgunit  14407  issubrg2  14409  aprap  14458  lsssn0  14567  islss3  14576  sralmod  14647  restopnb  15095  icnpimaex  15125  cnptopresti  15152  psmettri  15244  isxmet2d  15262  xmettri  15286  metrtri  15291  xmetres2  15293  bldisj  15315  blss2ps  15320  blss2  15321  xmstri2  15384  mstri2  15385  xmstri  15386  mstri  15387  xmstri3  15388  mstri3  15389  msrtri  15390  comet  15413  bdbl  15417  xmetxp  15421  dvconst  15608  dvconstre  15610  dvconstss  15612  sgmmul  15913  gausslemma2dlem1a  15980  pw1ndom3  16813