Theorem simpr1 1003

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

Assertion

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

Proof of Theorem simpr1

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

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

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 980

This theorem is referenced by:  simplr1  1039  simprr1  1045  simp1r1  1093  simp2r1  1099  simp3r1  1105  3anandis  1347  isopolem  5823  caovlem2d  6067  tfrlemibacc  6327  tfrlemibfn  6329  tfr1onlembacc  6343  tfr1onlembfn  6345  tfrcllembacc  6356  tfrcllembfn  6358  eqsupti  6995  prmuloc2  7566  ltntri  8085  elioc2  9936  elico2  9937  elicc2  9938  fseq1p1m1  10094  elfz0ubfz0  10125  ico0  10262  seq3f1olemp  10502  seq3f1oleml  10503  bcval5  10743  isumss2  11401  tanaddap  11747  dvds2ln  11831  divalglemeunn  11926  divalglemex  11927  divalglemeuneg  11928  qredeq  12096  pcdvdstr  12326  isstructr  12477  mndissubm  12866  grpsubrcan  12951  grpsubadd  12958  grpsubsub  12959  grpaddsubass  12960  grpsubsub4  12963  grpnnncan2  12967  mulgnndir  13012  mulgnn0dir  13013  mulgdir  13015  mulgnnass  13018  mulgnn0ass  13019  mulgass  13020  mulgsubdir  13023  issubg2m  13049  eqgval  13082  cmn32  13107  cmn12  13109  abladdsub  13118  srgass  13154  ringdilem  13195  ringass  13199  opprring  13249  mulgass3  13254  unitgrp  13285  dvrass  13308  dvrdir  13312  subrgunit  13360  issubrg2  13362  aprap  13376  icnpimaex  13714  cnptopresti  13741  upxp  13775  psmettri  13833  isxmet2d  13851  xmettri  13875  metrtri  13880  xmetres2  13882  bldisj  13904  blss2ps  13909  blss2  13910  xmstri2  13973  mstri2  13974  xmstri  13975  mstri  13976  xmstri3  13977  mstri3  13978  msrtri  13979  comet  14002  bdbl  14006  xmetxp  14010  dvconst  14164  findset  14700