Theorem simp33r 1308

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

Assertion

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

Proof of Theorem simp33r

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  totprob  34618  cdleme19b  40803  cdleme19e  40806  cdleme20h  40815  cdleme20l2  40820  cdleme20m  40822  cdleme21d  40829  cdleme21e  40830  cdleme22eALTN  40844  cdleme22f2  40846  cdleme22g  40847  cdleme26e  40858  cdleme37m  40961  cdlemeg46gfre  41031  cdlemg28a  41192  cdlemg28b  41202  cdlemk5a  41334  cdlemk6  41336