Theorem simp31l 1289

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

Assertion

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

Proof of Theorem simp31l

Step	Hyp	Ref	Expression
1		simp1l 1190	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)
2	1	3ad2ant3 1128	1 ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑)

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

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  ps-2c  36214  cdlema1N  36477  trlval3  36873  cdleme12  36957  cdlemednpq  36985  cdleme19d  36992  cdleme19e  36993  cdleme20f  37000  cdleme20h  37002  cdleme20l2  37007  cdleme20l  37008  cdleme20m  37009  cdleme21j  37022  cdleme22a  37026  cdleme22cN  37028  cdleme22f2  37033  cdleme32b  37128  cdlemg12f  37334  cdlemg12g  37335  cdlemg12  37336  cdlemg28a  37379  cdlemg31b0N  37380  cdlemg29  37391  cdlemg33a  37392  cdlemg36  37400  cdlemg42  37415  cdlemk16a  37542  cdlemk21-2N  37577  cdlemk32  37583  cdlemkid2  37610  cdlemk54  37644  cdlemk55a  37645  dihord10  37909