Theorem simpl3 909

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

Assertion

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

Proof of Theorem simpl3

Step	Hyp	Ref	Expression
1		simp3 906	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	adantr 261	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:  simpll3  945  simprl3  951  simp1l3  999  simp2l3  1005  simp3l3  1011  3anandirs  1238  frirrg  4087  fcofo  5424  acexmid  5511  oawordi  6049  nnmord  6090  nnmword  6091  fidifsnen  6331  dif1en  6337  ac6sfi  6352  enq0tr  6532  distrlem4prl  6682  distrlem4pru  6683  ltaprg  6717  lelttr  7106  ltletr  7107  readdcan  7153  addcan  7191  addcan2  7192  ltadd2  7416  xrlelttr  8722  xrltletr  8723  icoshftf1o  8859  difelfzle  8992  fzo1fzo0n0  9039  ltexp2a  9306  exple1  9310  expnlbnd2  9374  addcn2  9831  mulcn2  9833