Theorem simp21r 1310

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

Assertion

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

Proof of Theorem simp21r

Step	Hyp	Ref	Expression
1		simp1r 1217	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	3ad2ant2 1152	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  modexp  14362  segconeu  36746  4atlem10  40631  lplncvrlvol2  40640  4atex  41101  4atex2-0cOLDN  41105  cdleme0moN  41250  cdleme16e  41307  cdleme17d1  41314  cdleme18d  41320  cdleme19d  41331  cdleme20f  41339  cdleme20g  41340  cdleme21ct  41354  cdleme22aa  41364  cdleme22cN  41367  cdleme22d  41368  cdleme22e  41369  cdleme22eALTN  41370  cdleme26e  41384  cdleme32e  41470  cdleme32f  41471  cdlemg4  41642  cdlemg18d  41706  cdlemg18  41707  cdlemg19a  41708  cdlemg19  41709  cdlemg21  41711  cdlemg33b0  41726  cdlemk5  41861  cdlemk6  41862  cdlemk7  41873  cdlemk11  41874  cdlemk12  41875  cdlemk21N  41898  cdlemk20  41899  cdlemk28-3  41933  cdlemk34  41935  cdlemkfid3N  41950  cdlemk55u1  41990