Theorem simp32l 1297

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

Assertion

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

Proof of Theorem simp32l

Step	Hyp	Ref	Expression
1		simp2l 1198	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜑)
2	1	3ad2ant3 1134	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:  cdlema1N  39774  paddasslem15  39817  4atex2-0aOLDN  40061  4atex3  40064  trlval3  40170  cdleme12  40254  cdleme19b  40287  cdleme19d  40289  cdleme19e  40290  cdleme20d  40295  cdleme20f  40297  cdleme20g  40298  cdleme21d  40313  cdleme21e  40314  cdleme21f  40315  cdleme22cN  40325  cdleme22e  40327  cdleme22f2  40330  cdleme22g  40331  cdleme26e  40342  cdleme28a  40353  cdleme37m  40445  cdleme39n  40449  cdlemg28b  40686  cdlemk3  40816  cdlemk12  40833  cdlemk12u  40855  cdlemkoatnle-2N  40858  cdlemk13-2N  40859  cdlemkole-2N  40860  cdlemk14-2N  40861  cdlemk15-2N  40862  cdlemk16-2N  40863  cdlemk17-2N  40864  cdlemk18-2N  40869  cdlemk19-2N  40870  cdlemk7u-2N  40871  cdlemk11u-2N  40872  cdlemk20-2N  40875  cdlemk30  40877  cdlemk23-3  40885  cdlemk24-3  40886