Theorem simp31r 1295

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

Assertion

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

Proof of Theorem simp31r

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  ps-2c  37469  cdlema1N  37732  cdlemednpq  38240  cdleme19e  38248  cdleme20h  38257  cdleme20j  38259  cdleme20l2  38262  cdleme20m  38264  cdleme22a  38281  cdleme22cN  38283  cdleme22f2  38288  cdleme26f2ALTN  38305  cdleme37m  38403  cdlemg12f  38589  cdlemg12g  38590  cdlemg12  38591  cdlemg28a  38634  cdlemg29  38646  cdlemg33a  38647  cdlemg36  38655  cdlemk16a  38797  cdlemk21-2N  38832  cdlemk54  38899  dihord10  39164