Theorem simp33r 1182

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

Assertion

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

Proof of Theorem simp33r

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  totprob  29816  cdleme19b  34610  cdleme19e  34613  cdleme20h  34622  cdleme20l2  34627  cdleme20m  34629  cdleme21d  34636  cdleme21e  34637  cdleme22eALTN  34651  cdleme22f2  34653  cdleme22g  34654  cdleme26e  34665  cdleme37m  34768  cdlemeg46gfre  34838  cdlemg28a  34999  cdlemg28b  35009  cdlemk5a  35141  cdlemk6  35143