Theorem simpr1 1006

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

Assertion

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

Proof of Theorem simpr1

Step	Hyp	Ref	Expression
1		simp1 1000	. 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:  simplr1  1042  simprr1  1048  simp1r1  1096  simp2r1  1102  simp3r1  1108  3anandis  1360  isopolem  5898  caovlem2d  6146  tfrlemibacc  6419  tfrlemibfn  6421  tfr1onlembacc  6435  tfr1onlembfn  6437  tfrcllembacc  6448  tfrcllembfn  6450  eqsupti  7105  prmuloc2  7687  ltntri  8207  elioc2  10065  elico2  10066  elicc2  10067  fseq1p1m1  10223  elfz0ubfz0  10254  ico0  10411  seq3f1olemp  10667  seq3f1oleml  10668  bcval5  10915  swrdsbslen  11127  ccatswrd  11131  isumss2  11748  tanaddap  12094  dvds2ln  12179  divalglemeunn  12276  divalglemex  12277  divalglemeuneg  12278  qredeq  12462  pcdvdstr  12694  isstructr  12891  prdssgrpd  13291  prdsmndd  13324  imasmnd2  13328  mndissubm  13351  grpsubrcan  13457  grpsubadd  13464  grpsubsub  13465  grpaddsubass  13466  grpsubsub4  13469  grpnnncan2  13473  imasgrp2  13490  mulgnndir  13531  mulgnn0dir  13532  mulgdir  13534  mulgnnass  13537  mulgnn0ass  13538  mulgass  13539  mulgsubdir  13542  issubg2m  13569  eqgval  13603  qusgrp  13612  kerf1ghm  13654  cmn32  13684  cmn12  13686  abladdsub  13695  rngass  13745  imasrng  13762  srgass  13777  ringdilem  13818  ringass  13822  imasring  13870  opprrng  13883  opprring  13885  mulgass3  13891  unitgrp  13922  dvrass  13945  dvrdir  13949  subrgunit  14045  issubrg2  14047  aprap  14092  islss3  14185  sralmod  14256  icnpimaex  14727  cnptopresti  14754  upxp  14788  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  findset  15955