Theorem simpr2 911

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

Assertion

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

Proof of Theorem simpr2

Step	Hyp	Ref	Expression
1		simp2 905	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜒)
2	1	adantl 262	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  simplr2  947  simprr2  953  simp1r2  1001  simp2r2  1007  simp3r2  1013  3anandis  1237  isopolem  5461  tfrlemibacc  5940  tfrlemibfn  5942  prltlu  6585  prdisj  6590  prmuloc2  6665  eluzuzle  8481  elioc2  8805  elico2  8806  elicc2  8807  fseq1p1m1  8956  fz0fzelfz0  8984