Theorem simpr1 944

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

Assertion

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

Proof of Theorem simpr1

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

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  simplr1  980  simprr1  986  simp1r1  1034  simp2r1  1040  simp3r1  1046  3anandis  1278  isopolem  5481  caovlem2d  5713  tfrlemibacc  5963  tfrlemibfn  5965  eqsupti  6409  prmuloc2  6757  elioc2  8959  elico2  8960  elicc2  8961  fseq1p1m1  9111  elfz0ubfz0  9136  ico0  9270  ibcval5  9690  dvds2ln  10228  divalglemeunn  10321  divalglemex  10322  divalglemeuneg  10323  qredeq  10478  findset  10740