Theorem simp33r 1303

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

Assertion

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

Proof of Theorem simp33r

Step	Hyp	Ref	Expression
1		simp3r 1204	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant3 1137	1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜓)

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

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 1091

This theorem is referenced by:  totprob  32106  cdleme19b  38055  cdleme19e  38058  cdleme20h  38067  cdleme20l2  38072  cdleme20m  38074  cdleme21d  38081  cdleme21e  38082  cdleme22eALTN  38096  cdleme22f2  38098  cdleme22g  38099  cdleme26e  38110  cdleme37m  38213  cdlemeg46gfre  38283  cdlemg28a  38444  cdlemg28b  38454  cdlemk5a  38586  cdlemk6  38588