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 394   ∧ 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 206  df-an 395  df-3an 1086

This theorem is referenced by:  ps-2c  39131  cdlema1N  39394  cdlemednpq  39902  cdleme19e  39910  cdleme20h  39919  cdleme20j  39921  cdleme20l2  39924  cdleme20m  39926  cdleme22a  39943  cdleme22cN  39945  cdleme22f2  39950  cdleme26f2ALTN  39967  cdleme37m  40065  cdlemg12f  40251  cdlemg12g  40252  cdlemg12  40253  cdlemg28a  40296  cdlemg29  40308  cdlemg33a  40309  cdlemg36  40317  cdlemk16a  40459  cdlemk21-2N  40494  cdlemk54  40561  dihord10  40826