Theorem simplr2 1064

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

Assertion

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

Proof of Theorem simplr2

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

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

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 1004

This theorem is referenced by:  prarloclemlt  7706  prarloclemlo  7707  seq3f1oleml  10771  ccatswrd  11244  resqrexlemdecn  11566  pcdvdstr  12893  ennnfoneleminc  13025  prdssgrpd  13491  prdsmndd  13524  grprcan  13613  mulgnn0dir  13732  lmodprop2d  14355  lssintclm  14391  psrbaglesuppg  14679  restopnb  14898  cnptopresti  14955  blsscls2  15210