Theorem simplr2 1067

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

Assertion

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

Proof of Theorem simplr2

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

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

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 1007

This theorem is referenced by:  prarloclemlt  7807  prarloclemlo  7808  seq3f1oleml  10877  ccatswrd  11358  resqrexlemdecn  11693  pcdvdstr  13021  ennnfoneleminc  13154  prdssgrpd  13620  prdsmndd  13653  grprcan  13742  mulgnn0dir  13861  lmodprop2d  14488  lssintclm  14524  psrbaglesuppg  14813  restopnb  15038  cnptopresti  15095  blsscls2  15350