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  14385  segconeu  36868  4atlem10  40756  lplncvrlvol2  40765  4atex  41226  4atex2-0cOLDN  41230  cdleme0moN  41375  cdleme16e  41432  cdleme17d1  41439  cdleme18d  41445  cdleme19d  41456  cdleme20f  41464  cdleme20g  41465  cdleme21ct  41479  cdleme22aa  41489  cdleme22cN  41492  cdleme22d  41493  cdleme22e  41494  cdleme22eALTN  41495  cdleme26e  41509  cdleme32e  41595  cdleme32f  41596  cdlemg4  41767  cdlemg18d  41831  cdlemg18  41832  cdlemg19a  41833  cdlemg19  41834  cdlemg21  41836  cdlemg33b0  41851  cdlemk5  41986  cdlemk6  41987  cdlemk7  41998  cdlemk11  41999  cdlemk12  42000  cdlemk21N  42023  cdlemk20  42024  cdlemk28-3  42058  cdlemk34  42060  cdlemkfid3N  42075  cdlemk55u1  42115