Theorem simp33l 1296

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

Assertion

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

Proof of Theorem simp33l

Step	Hyp	Ref	Expression
1		simp3l 1197	. 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:  totprob  31685  cdleme19b  37455  cdleme19d  37457  cdleme19e  37458  cdleme20h  37467  cdleme20l2  37472  cdleme20m  37474  cdleme21d  37481  cdleme21e  37482  cdleme22e  37495  cdleme22f2  37498  cdleme22g  37499  cdleme26e  37510  cdleme28a  37521  cdleme28b  37522  cdleme37m  37613  cdleme39n  37617  cdlemeg46gfre  37683  cdlemg28a  37844  cdlemg28b  37854  cdlemk3  37984  cdlemk5a  37986  cdlemk6  37988  cdlemkuat  38017  cdlemkid2  38075