Theorem simp31r 1296

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

Assertion

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

Proof of Theorem simp31r

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ps-2c  37542  cdlema1N  37805  cdlemednpq  38313  cdleme19e  38321  cdleme20h  38330  cdleme20j  38332  cdleme20l2  38335  cdleme20m  38337  cdleme22a  38354  cdleme22cN  38356  cdleme22f2  38361  cdleme26f2ALTN  38378  cdleme37m  38476  cdlemg12f  38662  cdlemg12g  38663  cdlemg12  38664  cdlemg28a  38707  cdlemg29  38719  cdlemg33a  38720  cdlemg36  38728  cdlemk16a  38870  cdlemk21-2N  38905  cdlemk54  38972  dihord10  39237