Theorem simp31l 1309

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

Assertion

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

Proof of Theorem simp31l

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  ps-2c  40116  cdlema1N  40379  trlval3  40775  cdleme12  40859  cdlemednpq  40887  cdleme19d  40894  cdleme19e  40895  cdleme20f  40902  cdleme20h  40904  cdleme20l2  40909  cdleme20l  40910  cdleme20m  40911  cdleme21j  40924  cdleme22a  40928  cdleme22cN  40930  cdleme22f2  40935  cdleme32b  41030  cdlemg12f  41236  cdlemg12g  41237  cdlemg12  41238  cdlemg28a  41281  cdlemg31b0N  41282  cdlemg29  41293  cdlemg33a  41294  cdlemg36  41302  cdlemg42  41317  cdlemk16a  41444  cdlemk21-2N  41479  cdlemk32  41485  cdlemkid2  41512  cdlemk54  41546  cdlemk55a  41547  dihord10  41811