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  5869  caovlem2d  6116  tfrlemibacc  6384  tfrlemibfn  6386  tfr1onlembacc  6400  tfr1onlembfn  6402  tfrcllembacc  6413  tfrcllembfn  6415  eqsupti  7062  prmuloc2  7634  ltntri  8154  elioc2  10011  elico2  10012  elicc2  10013  fseq1p1m1  10169  elfz0ubfz0  10200  ico0  10351  seq3f1olemp  10607  seq3f1oleml  10608  bcval5  10855  isumss2  11558  tanaddap  11904  dvds2ln  11989  divalglemeunn  12086  divalglemex  12087  divalglemeuneg  12088  qredeq  12264  pcdvdstr  12496  isstructr  12693  mndissubm  13107  grpsubrcan  13213  grpsubadd  13220  grpsubsub  13221  grpaddsubass  13222  grpsubsub4  13225  grpnnncan2  13229  imasgrp2  13240  mulgnndir  13281  mulgnn0dir  13282  mulgdir  13284  mulgnnass  13287  mulgnn0ass  13288  mulgass  13289  mulgsubdir  13292  issubg2m  13319  eqgval  13353  qusgrp  13362  kerf1ghm  13404  cmn32  13434  cmn12  13436  abladdsub  13445  rngass  13495  imasrng  13512  srgass  13527  ringdilem  13568  ringass  13572  imasring  13620  opprrng  13633  opprring  13635  mulgass3  13641  unitgrp  13672  dvrass  13695  dvrdir  13699  subrgunit  13795  issubrg2  13797  aprap  13842  islss3  13935  sralmod  14006  icnpimaex  14447  cnptopresti  14474  upxp  14508  psmettri  14566  isxmet2d  14584  xmettri  14608  metrtri  14613  xmetres2  14615  bldisj  14637  blss2ps  14642  blss2  14643  xmstri2  14706  mstri2  14707  xmstri  14708  mstri  14709  xmstri3  14710  mstri3  14711  msrtri  14712  comet  14735  bdbl  14739  xmetxp  14743  dvconst  14930  dvconstre  14932  dvconstss  14934  sgmmul  15232  findset  15591