Theorem simpr1 988

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

Assertion

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

Proof of Theorem simpr1

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

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  simplr1  1024  simprr1  1030  simp1r1  1078  simp2r1  1084  simp3r1  1090  3anandis  1326  isopolem  5731  caovlem2d  5971  tfrlemibacc  6231  tfrlemibfn  6233  tfr1onlembacc  6247  tfr1onlembfn  6249  tfrcllembacc  6260  tfrcllembfn  6262  eqsupti  6891  prmuloc2  7399  ltntri  7914  elioc2  9749  elico2  9750  elicc2  9751  fseq1p1m1  9905  elfz0ubfz0  9933  ico0  10070  seq3f1olemp  10306  seq3f1oleml  10307  bcval5  10541  isumss2  11194  tanaddap  11482  dvds2ln  11562  divalglemeunn  11654  divalglemex  11655  divalglemeuneg  11656  qredeq  11813  isstructr  12013  icnpimaex  12419  cnptopresti  12446  upxp  12480  psmettri  12538  isxmet2d  12556  xmettri  12580  metrtri  12585  xmetres2  12587  bldisj  12609  blss2ps  12614  blss2  12615  xmstri2  12678  mstri2  12679  xmstri  12680  mstri  12681  xmstri3  12682  mstri3  12683  msrtri  12684  comet  12707  bdbl  12711  xmetxp  12715  dvconst  12869  findset  13314