Theorem simp31l 1292

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

Assertion

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

Proof of Theorem simp31l

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  ps-2c  36679  cdlema1N  36942  trlval3  37338  cdleme12  37422  cdlemednpq  37450  cdleme19d  37457  cdleme19e  37458  cdleme20f  37465  cdleme20h  37467  cdleme20l2  37472  cdleme20l  37473  cdleme20m  37474  cdleme21j  37487  cdleme22a  37491  cdleme22cN  37493  cdleme22f2  37498  cdleme32b  37593  cdlemg12f  37799  cdlemg12g  37800  cdlemg12  37801  cdlemg28a  37844  cdlemg31b0N  37845  cdlemg29  37856  cdlemg33a  37857  cdlemg36  37865  cdlemg42  37880  cdlemk16a  38007  cdlemk21-2N  38042  cdlemk32  38048  cdlemkid2  38075  cdlemk54  38109  cdlemk55a  38110  dihord10  38374