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  7620  prarloclemlt  7860  prarloclemlo  7861  ccatswrd  11444  pfxccat3  11508  resqrexlemdecn  11780  summodclem2  12151  isumss2  12162  pcdvdstr  13108  ennnfoneleminc  13304  grprcan  13844  mulgnn0dir  13957  mulgdir  13959  mulgass  13964  prdssgrpd  14193  prdsmndd  14196  lmodprop2d  14687  lssintclm  14723  psrbaglesuppg  15059  restopnb  15284  blsscls2  15596