Theorem simp32l 1299

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

Assertion

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

Proof of Theorem simp32l

Step	Hyp	Ref	Expression
1		simp2l 1200	. 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:  cdlema1N  39770  paddasslem15  39813  4atex2-0aOLDN  40057  4atex3  40060  trlval3  40166  cdleme12  40250  cdleme19b  40283  cdleme19d  40285  cdleme19e  40286  cdleme20d  40291  cdleme20f  40293  cdleme20g  40294  cdleme21d  40309  cdleme21e  40310  cdleme21f  40311  cdleme22cN  40321  cdleme22e  40323  cdleme22f2  40326  cdleme22g  40327  cdleme26e  40338  cdleme28a  40349  cdleme37m  40441  cdleme39n  40445  cdlemg28b  40682  cdlemk3  40812  cdlemk12  40829  cdlemk12u  40851  cdlemkoatnle-2N  40854  cdlemk13-2N  40855  cdlemkole-2N  40856  cdlemk14-2N  40857  cdlemk15-2N  40858  cdlemk16-2N  40859  cdlemk17-2N  40860  cdlemk18-2N  40865  cdlemk19-2N  40866  cdlemk7u-2N  40867  cdlemk11u-2N  40868  cdlemk20-2N  40871  cdlemk30  40873  cdlemk23-3  40881  cdlemk24-3  40882