Theorem simp21r 1301

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

Assertion

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

Proof of Theorem simp21r

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1095

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 209  df-an 399  df-3an 1097

This theorem is referenced by:  modexp  14237  segconeu  36299  4atlem10  40168  lplncvrlvol2  40177  4atex  40638  4atex2-0cOLDN  40642  cdleme0moN  40787  cdleme16e  40844  cdleme17d1  40851  cdleme18d  40857  cdleme19d  40868  cdleme20f  40876  cdleme20g  40877  cdleme21ct  40891  cdleme22aa  40901  cdleme22cN  40904  cdleme22d  40905  cdleme22e  40906  cdleme22eALTN  40907  cdleme26e  40921  cdleme32e  41007  cdleme32f  41008  cdlemg4  41179  cdlemg18d  41243  cdlemg18  41244  cdlemg19a  41245  cdlemg19  41246  cdlemg21  41248  cdlemg33b0  41263  cdlemk5  41398  cdlemk6  41399  cdlemk7  41410  cdlemk11  41411  cdlemk12  41412  cdlemk21N  41435  cdlemk20  41436  cdlemk28-3  41470  cdlemk34  41472  cdlemkfid3N  41487  cdlemk55u1  41527