Theorem simplr3 1072

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

Assertion

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

Proof of Theorem simplr3

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  netap  7627  prarloclemlt  7867  prarloclemlo  7868  ccatswrd  11465  pfxccat3  11529  resqrexlemdecn  11801  summodclem2  12175  isumss2  12186  pcdvdstr  13136  ennnfoneleminc  13361  grprcan  13902  mulgnn0dir  14015  mulgdir  14017  mulgass  14022  prdssgrpd  14299  prdsmndd  14302  lmodprop2d  14795  lssintclm  14831  psrbaglesuppg  15172  restopnb  15419  blsscls2  15731