Theorem simplr2 1071

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

Assertion

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

Proof of Theorem simplr2

Step	Hyp	Ref	Expression
1		simpr2 1035	. 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:  prarloclemlt  7861  prarloclemlo  7862  seq3f1oleml  10967  ccatswrd  11457  resqrexlemdecn  11793  pcdvdstr  13128  ennnfoneleminc  13353  grprcan  13893  mulgnn0dir  14006  prdssgrpd  14242  prdsmndd  14245  lmodprop2d  14736  lssintclm  14772  psrbaglesuppg  15108  restopnb  15334  cnptopresti  15391  blsscls2  15646