Theorem simp21r 1287

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

Assertion

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

Proof of Theorem simp21r

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

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

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 1085

This theorem is referenced by:  modexp  13598  segconeu  33472  4atlem10  36741  lplncvrlvol2  36750  4atex  37211  4atex2-0cOLDN  37215  cdleme0moN  37360  cdleme16e  37417  cdleme17d1  37424  cdleme18d  37430  cdleme19d  37441  cdleme20f  37449  cdleme20g  37450  cdleme21ct  37464  cdleme22aa  37474  cdleme22cN  37477  cdleme22d  37478  cdleme22e  37479  cdleme22eALTN  37480  cdleme26e  37494  cdleme32e  37580  cdleme32f  37581  cdlemg4  37752  cdlemg18d  37816  cdlemg18  37817  cdlemg19a  37818  cdlemg19  37819  cdlemg21  37821  cdlemg33b0  37836  cdlemk5  37971  cdlemk6  37972  cdlemk7  37983  cdlemk11  37984  cdlemk12  37985  cdlemk21N  38008  cdlemk20  38009  cdlemk28-3  38043  cdlemk34  38045  cdlemkfid3N  38060  cdlemk55u1  38100