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  14163  segconeu  35987  4atlem10  39588  lplncvrlvol2  39597  4atex  40058  4atex2-0cOLDN  40062  cdleme0moN  40207  cdleme16e  40264  cdleme17d1  40271  cdleme18d  40277  cdleme19d  40288  cdleme20f  40296  cdleme20g  40297  cdleme21ct  40311  cdleme22aa  40321  cdleme22cN  40324  cdleme22d  40325  cdleme22e  40326  cdleme22eALTN  40327  cdleme26e  40341  cdleme32e  40427  cdleme32f  40428  cdlemg4  40599  cdlemg18d  40663  cdlemg18  40664  cdlemg19a  40665  cdlemg19  40666  cdlemg21  40668  cdlemg33b0  40683  cdlemk5  40818  cdlemk6  40819  cdlemk7  40830  cdlemk11  40831  cdlemk12  40832  cdlemk21N  40855  cdlemk20  40856  cdlemk28-3  40890  cdlemk34  40892  cdlemkfid3N  40907  cdlemk55u1  40947