Theorem simp33l 1297

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

Assertion

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

Proof of Theorem simp33l

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  totprob  31795  cdleme19b  37600  cdleme19d  37602  cdleme19e  37603  cdleme20h  37612  cdleme20l2  37617  cdleme20m  37619  cdleme21d  37626  cdleme21e  37627  cdleme22e  37640  cdleme22f2  37643  cdleme22g  37644  cdleme26e  37655  cdleme28a  37666  cdleme28b  37667  cdleme37m  37758  cdleme39n  37762  cdlemeg46gfre  37828  cdlemg28a  37989  cdlemg28b  37999  cdlemk3  38129  cdlemk5a  38131  cdlemk6  38133  cdlemkuat  38162  cdlemkid2  38220