Theorem simp23r 1297

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

Assertion

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

Proof of Theorem simp23r

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  ax5seglem6  26979  lshpkrlem5  36814  lplnexllnN  37264  4atexlemutvt  37754  cdlemc5  37895  cdlemd2  37899  cdleme0moN  37925  cdleme3h  37935  cdleme5  37940  cdleme9  37953  cdleme11l  37969  cdleme14  37973  cdleme15c  37976  cdleme16b  37979  cdleme16d  37981  cdleme16e  37982  cdlemednpq  37999  cdleme20bN  38010  cdleme20j  38018  cdleme20l2  38021  cdleme20l  38022  cdleme22cN  38042  cdleme22d  38043  cdleme22e  38044  cdleme22f  38046  cdleme26fALTN  38062  cdleme26f  38063  cdleme26f2ALTN  38064  cdleme26f2  38065  cdleme27a  38067  cdleme32b  38142  cdleme32d  38144  cdleme32f  38146  cdleme39n  38166  cdleme40n  38168  cdlemg2fv2  38300  cdlemg17h  38368  cdlemg27b  38396  cdlemg28b  38403  cdlemg28  38404  cdlemg29  38405  cdlemg33a  38406  cdlemg33d  38409  cdlemk7u-2N  38588  cdlemk11u-2N  38589  cdlemk12u-2N  38590  cdlemk26-3  38606  cdlemk27-3  38607  cdlemkfid3N  38625  cdlemn11c  38909