Theorem simp31l 1315

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

Assertion

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

Proof of Theorem simp31l

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ps-2c  40343  cdlema1N  40606  trlval3  41002  cdleme12  41086  cdlemednpq  41114  cdleme19d  41121  cdleme19e  41122  cdleme20f  41129  cdleme20h  41131  cdleme20l2  41136  cdleme20l  41137  cdleme20m  41138  cdleme21j  41151  cdleme22a  41155  cdleme22cN  41157  cdleme22f2  41162  cdleme32b  41257  cdlemg12f  41463  cdlemg12g  41464  cdlemg12  41465  cdlemg28a  41508  cdlemg31b0N  41509  cdlemg29  41520  cdlemg33a  41521  cdlemg36  41529  cdlemg42  41544  cdlemk16a  41671  cdlemk21-2N  41706  cdlemk32  41712  cdlemkid2  41739  cdlemk54  41773  cdlemk55a  41774  dihord10  42038