Theorem simp22r 1295

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

Assertion

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

Proof of Theorem simp22r

Step	Hyp	Ref	Expression
1		simp2r 1202	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓)
2	1	3ad2ant2 1135	1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  frrlem10  8245  ttrclselem2  9647  ax5seglem6  29003  segconeu  36193  3atlem2  39930  lplnexllnN  40010  lplncvrlvol2  40061  4atex  40522  cdleme3g  40680  cdleme3h  40681  cdleme11h  40712  cdleme20bN  40756  cdleme20c  40757  cdleme20f  40760  cdleme20g  40761  cdleme20j  40764  cdleme20l2  40767  cdleme20l  40768  cdleme21ct  40775  cdleme26e  40805  cdleme43fsv1snlem  40866  cdleme39n  40912  cdleme40m  40913  cdleme42k  40930  cdlemg6c  41066  cdlemg31d  41146  cdlemg33a  41152  cdlemg33c  41154  cdlemg33d  41155  cdlemg33e  41156  cdlemg33  41157  cdlemh  41263  cdlemk7u-2N  41334  cdlemk11u-2N  41335  cdlemk12u-2N  41336  cdlemk20-2N  41338  cdlemk28-3  41354  cdlemk33N  41355  cdlemk34  41356  cdlemk39  41362  cdlemkyyN  41408