Theorem simp23r 1293

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

Assertion

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

Proof of Theorem simp23r

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

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

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 396  df-3an 1087

This theorem is referenced by:  ax5seglem6  27283  lshpkrlem5  37107  lplnexllnN  37557  4atexlemutvt  38047  cdlemc5  38188  cdlemd2  38192  cdleme0moN  38218  cdleme3h  38228  cdleme5  38233  cdleme9  38246  cdleme11l  38262  cdleme14  38266  cdleme15c  38269  cdleme16b  38272  cdleme16d  38274  cdleme16e  38275  cdlemednpq  38292  cdleme20bN  38303  cdleme20j  38311  cdleme20l2  38314  cdleme20l  38315  cdleme22cN  38335  cdleme22d  38336  cdleme22e  38337  cdleme22f  38339  cdleme26fALTN  38355  cdleme26f  38356  cdleme26f2ALTN  38357  cdleme26f2  38358  cdleme27a  38360  cdleme32b  38435  cdleme32d  38437  cdleme32f  38439  cdleme39n  38459  cdleme40n  38461  cdlemg2fv2  38593  cdlemg17h  38661  cdlemg27b  38689  cdlemg28b  38696  cdlemg28  38697  cdlemg29  38698  cdlemg33a  38699  cdlemg33d  38702  cdlemk7u-2N  38881  cdlemk11u-2N  38882  cdlemk12u-2N  38883  cdlemk26-3  38899  cdlemk27-3  38900  cdlemkfid3N  38918  cdlemn11c  39202