Theorem simpr1 1005

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

Assertion

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

Proof of Theorem simpr1

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

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

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 982

This theorem is referenced by:  simplr1  1041  simprr1  1047  simp1r1  1095  simp2r1  1101  simp3r1  1107  3anandis  1358  isopolem  5872  caovlem2d  6120  tfrlemibacc  6393  tfrlemibfn  6395  tfr1onlembacc  6409  tfr1onlembfn  6411  tfrcllembacc  6422  tfrcllembfn  6424  eqsupti  7071  prmuloc2  7653  ltntri  8173  elioc2  10030  elico2  10031  elicc2  10032  fseq1p1m1  10188  elfz0ubfz0  10219  ico0  10370  seq3f1olemp  10626  seq3f1oleml  10627  bcval5  10874  isumss2  11577  tanaddap  11923  dvds2ln  12008  divalglemeunn  12105  divalglemex  12106  divalglemeuneg  12107  qredeq  12291  pcdvdstr  12523  isstructr  12720  prdssgrpd  13119  prdsmndd  13152  imasmnd2  13156  mndissubm  13179  grpsubrcan  13285  grpsubadd  13292  grpsubsub  13293  grpaddsubass  13294  grpsubsub4  13297  grpnnncan2  13301  imasgrp2  13318  mulgnndir  13359  mulgnn0dir  13360  mulgdir  13362  mulgnnass  13365  mulgnn0ass  13366  mulgass  13367  mulgsubdir  13370  issubg2m  13397  eqgval  13431  qusgrp  13440  kerf1ghm  13482  cmn32  13512  cmn12  13514  abladdsub  13523  rngass  13573  imasrng  13590  srgass  13605  ringdilem  13646  ringass  13650  imasring  13698  opprrng  13711  opprring  13713  mulgass3  13719  unitgrp  13750  dvrass  13773  dvrdir  13777  subrgunit  13873  issubrg2  13875  aprap  13920  islss3  14013  sralmod  14084  icnpimaex  14533  cnptopresti  14560  upxp  14594  psmettri  14652  isxmet2d  14670  xmettri  14694  metrtri  14699  xmetres2  14701  bldisj  14723  blss2ps  14728  blss2  14729  xmstri2  14792  mstri2  14793  xmstri  14794  mstri  14795  xmstri3  14796  mstri3  14797  msrtri  14798  comet  14821  bdbl  14825  xmetxp  14829  dvconst  15016  dvconstre  15018  dvconstss  15020  sgmmul  15318  findset  15677