Theorem simp33r 1302

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

Assertion

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

Proof of Theorem simp33r

Step	Hyp	Ref	Expression
1		simp3r 1203	. 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:  totprob  34394  cdleme19b  40283  cdleme19e  40286  cdleme20h  40295  cdleme20l2  40300  cdleme20m  40302  cdleme21d  40309  cdleme21e  40310  cdleme22eALTN  40324  cdleme22f2  40326  cdleme22g  40327  cdleme26e  40338  cdleme37m  40441  cdlemeg46gfre  40511  cdlemg28a  40672  cdlemg28b  40682  cdlemk5a  40814  cdlemk6  40816