Theorem simplr3 1067

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simplr3	⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒)

Proof of Theorem simplr3

Step	Hyp	Ref	Expression
1		simpr3 1031	. 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜒)
2	1	adantr 276	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  netap  7473  prarloclemlt  7713  prarloclemlo  7714  ccatswrd  11252  pfxccat3  11316  resqrexlemdecn  11574  summodclem2  11945  isumss2  11956  pcdvdstr  12902  ennnfoneleminc  13034  prdssgrpd  13500  prdsmndd  13533  grprcan  13622  mulgnn0dir  13741  mulgdir  13743  mulgass  13748  lmodprop2d  14365  lssintclm  14401  psrbaglesuppg  14689  restopnb  14908  blsscls2  15220