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  14203  segconeu  35999  4atlem10  39600  lplncvrlvol2  39609  4atex  40070  4atex2-0cOLDN  40074  cdleme0moN  40219  cdleme16e  40276  cdleme17d1  40283  cdleme18d  40289  cdleme19d  40300  cdleme20f  40308  cdleme20g  40309  cdleme21ct  40323  cdleme22aa  40333  cdleme22cN  40336  cdleme22d  40337  cdleme22e  40338  cdleme22eALTN  40339  cdleme26e  40353  cdleme32e  40439  cdleme32f  40440  cdlemg4  40611  cdlemg18d  40675  cdlemg18  40676  cdlemg19a  40677  cdlemg19  40678  cdlemg21  40680  cdlemg33b0  40695  cdlemk5  40830  cdlemk6  40831  cdlemk7  40842  cdlemk11  40843  cdlemk12  40844  cdlemk21N  40867  cdlemk20  40868  cdlemk28-3  40902  cdlemk34  40904  cdlemkfid3N  40919  cdlemk55u1  40959