Theorem simp31l 1297

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

Assertion

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

Proof of Theorem simp31l

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

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

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

This theorem is referenced by:  ps-2c  39784  cdlema1N  40047  trlval3  40443  cdleme12  40527  cdlemednpq  40555  cdleme19d  40562  cdleme19e  40563  cdleme20f  40570  cdleme20h  40572  cdleme20l2  40577  cdleme20l  40578  cdleme20m  40579  cdleme21j  40592  cdleme22a  40596  cdleme22cN  40598  cdleme22f2  40603  cdleme32b  40698  cdlemg12f  40904  cdlemg12g  40905  cdlemg12  40906  cdlemg28a  40949  cdlemg31b0N  40950  cdlemg29  40961  cdlemg33a  40962  cdlemg36  40970  cdlemg42  40985  cdlemk16a  41112  cdlemk21-2N  41147  cdlemk32  41153  cdlemkid2  41180  cdlemk54  41214  cdlemk55a  41215  dihord10  41479