Theorem simp31r 1294

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

Assertion

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

Proof of Theorem simp31r

Step	Hyp	Ref	Expression
1		simp1r 1195	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	3ad2ant3 1132	1 ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086

This theorem is referenced by:  ps-2c  36824  cdlema1N  37087  cdlemednpq  37595  cdleme19e  37603  cdleme20h  37612  cdleme20j  37614  cdleme20l2  37617  cdleme20m  37619  cdleme22a  37636  cdleme22cN  37638  cdleme22f2  37643  cdleme26f2ALTN  37660  cdleme37m  37758  cdlemg12f  37944  cdlemg12g  37945  cdlemg12  37946  cdlemg28a  37989  cdlemg29  38001  cdlemg33a  38002  cdlemg36  38010  cdlemk16a  38152  cdlemk21-2N  38187  cdlemk54  38254  dihord10  38519