Theorem simpr3 946

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

Assertion

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

Proof of Theorem simpr3

Step	Hyp	Ref	Expression
1		simp3 940	. 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:  simplr3  982  simprr3  988  simp1r3  1036  simp2r3  1042  simp3r3  1048  3anandis  1278  isopolem  5481  tfrlemibacc  5963  tfrlemibxssdm  5964  tfrlemibfn  5965  prloc  6681  prmuloc2  6757  eluzuzle  8627  elioc2  8959  elico2  8960  elicc2  8961  fseq1p1m1  9111  ibcval5  9690  dvds2ln  10228  divalglemeunn  10321  divalglemex  10322  divalglemeuneg  10323