Theorem simp33r 1320

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

Assertion

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

Proof of Theorem simp33r

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  totprob  34798  cdleme19b  41059  cdleme19e  41062  cdleme20h  41071  cdleme20l2  41076  cdleme20m  41078  cdleme21d  41085  cdleme21e  41086  cdleme22eALTN  41100  cdleme22f2  41102  cdleme22g  41103  cdleme26e  41114  cdleme37m  41217  cdlemeg46gfre  41287  cdlemg28a  41448  cdlemg28b  41458  cdlemk5a  41590  cdlemk6  41592