Theorem simp21r 1292

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

Assertion

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

Proof of Theorem simp21r

Step	Hyp	Ref	Expression
1		simp1r 1199	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	3ad2ant2 1134	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:  modexp  14147  segconeu  36076  4atlem10  39726  lplncvrlvol2  39735  4atex  40196  4atex2-0cOLDN  40200  cdleme0moN  40345  cdleme16e  40402  cdleme17d1  40409  cdleme18d  40415  cdleme19d  40426  cdleme20f  40434  cdleme20g  40435  cdleme21ct  40449  cdleme22aa  40459  cdleme22cN  40462  cdleme22d  40463  cdleme22e  40464  cdleme22eALTN  40465  cdleme26e  40479  cdleme32e  40565  cdleme32f  40566  cdlemg4  40737  cdlemg18d  40801  cdlemg18  40802  cdlemg19a  40803  cdlemg19  40804  cdlemg21  40806  cdlemg33b0  40821  cdlemk5  40956  cdlemk6  40957  cdlemk7  40968  cdlemk11  40969  cdlemk12  40970  cdlemk21N  40993  cdlemk20  40994  cdlemk28-3  41028  cdlemk34  41030  cdlemkfid3N  41045  cdlemk55u1  41085