Theorem simp33l 1384

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

Assertion

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

Proof of Theorem simp33l

Step	Hyp	Ref	Expression
1		simp3l 1243	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant3 1129	1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071

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 197  df-an 383  df-3an 1073

This theorem is referenced by:  totprob  30829  cdleme19b  36113  cdleme19d  36115  cdleme19e  36116  cdleme20h  36125  cdleme20l2  36130  cdleme20m  36132  cdleme21d  36139  cdleme21e  36140  cdleme22e  36153  cdleme22f2  36156  cdleme22g  36157  cdleme26e  36168  cdleme28a  36179  cdleme28b  36180  cdleme37m  36271  cdleme39n  36275  cdlemeg46gfre  36341  cdlemg28a  36502  cdlemg28b  36512  cdlemk3  36642  cdlemk5a  36644  cdlemk6  36646  cdlemkuat  36675  cdlemkid2  36733