Theorem simp23r 1295

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

Assertion

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

Proof of Theorem simp23r

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ 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 206  df-an 398  df-3an 1089

This theorem is referenced by:  ax5seglem6  27351  lshpkrlem5  37328  lplnexllnN  37778  4atexlemutvt  38268  cdlemc5  38409  cdlemd2  38413  cdleme0moN  38439  cdleme3h  38449  cdleme5  38454  cdleme9  38467  cdleme11l  38483  cdleme14  38487  cdleme15c  38490  cdleme16b  38493  cdleme16d  38495  cdleme16e  38496  cdlemednpq  38513  cdleme20bN  38524  cdleme20j  38532  cdleme20l2  38535  cdleme20l  38536  cdleme22cN  38556  cdleme22d  38557  cdleme22e  38558  cdleme22f  38560  cdleme26fALTN  38576  cdleme26f  38577  cdleme26f2ALTN  38578  cdleme26f2  38579  cdleme27a  38581  cdleme32b  38656  cdleme32d  38658  cdleme32f  38660  cdleme39n  38680  cdleme40n  38682  cdlemg2fv2  38814  cdlemg17h  38882  cdlemg27b  38910  cdlemg28b  38917  cdlemg28  38918  cdlemg29  38919  cdlemg33a  38920  cdlemg33d  38923  cdlemk7u-2N  39102  cdlemk11u-2N  39103  cdlemk12u-2N  39104  cdlemk26-3  39120  cdlemk27-3  39121  cdlemkfid3N  39139  cdlemn11c  39423