Theorem simpr3 912

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

Assertion

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

Proof of Theorem simpr3

Step	Hyp	Ref	Expression
1		simp3 906	. 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:  simplr3  948  simprr3  954  simp1r3  1002  simp2r3  1008  simp3r3  1014  3anandis  1237  isopolem  5461  tfrlemibacc  5940  tfrlemibxssdm  5941  tfrlemibfn  5942  prloc  6589  prmuloc2  6665  eluzuzle  8481  elioc2  8805  elico2  8806  elicc2  8807  fseq1p1m1  8956