Theorem simp33r 1189

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

Assertion

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

Proof of Theorem simp33r

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  totprob  30489  cdleme19b  35592  cdleme19e  35595  cdleme20h  35604  cdleme20l2  35609  cdleme20m  35611  cdleme21d  35618  cdleme21e  35619  cdleme22eALTN  35633  cdleme22f2  35635  cdleme22g  35636  cdleme26e  35647  cdleme37m  35750  cdlemeg46gfre  35820  cdlemg28a  35981  cdlemg28b  35991  cdlemk5a  36123  cdlemk6  36125