Theorem simpr2 945

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

Assertion

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

Proof of Theorem simpr2

Step	Hyp	Ref	Expression
1		simp2 939	. 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:  simplr2  981  simprr2  987  simp1r2  1035  simp2r2  1041  simp3r2  1047  3anandis  1278  isopolem  5481  tfrlemibacc  5963  tfrlemibfn  5965  prltlu  6677  prdisj  6682  prmuloc2  6757  eluzuzle  8627  elioc2  8959  elico2  8960  elicc2  8961  fseq1p1m1  9111  fz0fzelfz0  9138  ibcval5  9690  dvds2ln  10228  divalglemeunn  10321  divalglemex  10322  divalglemeuneg  10323