Theorem simp23r 1296

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

Assertion

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

Proof of Theorem simp23r

Step	Hyp	Ref	Expression
1		simp3r 1203	. 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:  ax5seglem6  28949  lshpkrlem5  39115  lplnexllnN  39566  4atexlemutvt  40056  cdlemc5  40197  cdlemd2  40201  cdleme0moN  40227  cdleme3h  40237  cdleme5  40242  cdleme9  40255  cdleme11l  40271  cdleme14  40275  cdleme15c  40278  cdleme16b  40281  cdleme16d  40283  cdleme16e  40284  cdlemednpq  40301  cdleme20bN  40312  cdleme20j  40320  cdleme20l2  40323  cdleme20l  40324  cdleme22cN  40344  cdleme22d  40345  cdleme22e  40346  cdleme22f  40348  cdleme26fALTN  40364  cdleme26f  40365  cdleme26f2ALTN  40366  cdleme26f2  40367  cdleme27a  40369  cdleme32b  40444  cdleme32d  40446  cdleme32f  40448  cdleme39n  40468  cdleme40n  40470  cdlemg2fv2  40602  cdlemg17h  40670  cdlemg27b  40698  cdlemg28b  40705  cdlemg28  40706  cdlemg29  40707  cdlemg33a  40708  cdlemg33d  40711  cdlemk7u-2N  40890  cdlemk11u-2N  40891  cdlemk12u-2N  40892  cdlemk26-3  40908  cdlemk27-3  40909  cdlemkfid3N  40927  cdlemn11c  41211