Theorem simp31r 1183

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

Assertion

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

Proof of Theorem simp31r

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036

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 197  df-an 386  df-3an 1038

This theorem is referenced by:  ps-2c  34291  cdlema1N  34554  cdlemednpq  35063  cdleme19e  35072  cdleme20h  35081  cdleme20j  35083  cdleme20l2  35086  cdleme20m  35088  cdleme22a  35105  cdleme22cN  35107  cdleme22f2  35112  cdleme26f2ALTN  35129  cdleme37m  35227  cdlemg12f  35413  cdlemg12g  35414  cdlemg12  35415  cdlemg28a  35458  cdlemg29  35470  cdlemg33a  35471  cdlemg36  35479  cdlemk16a  35621  cdlemk21-2N  35656  cdlemk54  35723  dihord10  35989