Theorem simp23l 1296

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

Assertion

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

Proof of Theorem simp23l

Step	Hyp	Ref	Expression
1		simp3l 1203	. 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  4atexlemt  37753  4atex2  37777  4atex3  37781  trlval4  37888  cdlemc5  37895  cdlemc6  37896  cdlemd2  37899  cdleme0e  37917  cdleme0moN  37925  cdleme3g  37934  cdleme3h  37935  cdleme3  37937  cdleme4  37938  cdleme5  37940  cdleme9  37953  cdleme11fN  37964  cdleme11j  37967  cdleme11k  37968  cdleme11l  37969  cdleme11  37970  cdleme14  37973  cdleme15a  37974  cdleme15b  37975  cdleme15c  37976  cdleme16b  37979  cdleme16c  37980  cdleme16d  37981  cdleme16e  37982  cdleme16f  37983  cdleme17d1  37989  cdleme18c  37993  cdlemednpq  37999  cdleme19c  38005  cdleme20bN  38010  cdleme20d  38012  cdleme20f  38014  cdleme20g  38015  cdleme20h  38016  cdleme20j  38018  cdleme20l2  38021  cdleme20l  38022  cdleme20m  38023  cdleme22cN  38042  cdleme22d  38043  cdleme22e  38044  cdleme22f  38046  cdleme26fALTN  38062  cdleme26f  38063  cdleme26f2ALTN  38064  cdleme26f2  38065  cdleme27a  38067  cdleme28a  38070  cdlemefs44  38126  cdlemefs45ee  38130  cdleme32b  38142  cdleme32c  38143  cdleme32e  38145  cdleme35sn2aw  38158  cdleme37m  38162  cdleme39n  38166  cdleme40n  38168  cdleme40w  38170  cdleme42k  38184  cdlemeg47rv2  38210  cdlemeg46rjgN  38222  cdlemeg46rgv  38228  cdlemeg46req  38229  cdlemg2fv2  38300  cdlemg17h  38368  cdlemg31b0a  38395  cdlemg27b  38396  cdlemg31d  38400  cdlemg28b  38403  cdlemg28  38404  cdlemg29  38405  cdlemg33a  38406  cdlemg33b  38407  cdlemg33c  38408  cdlemg33d  38409  cdlemg33e  38410  cdlemg44a  38431  cdlemk7u-2N  38588  cdlemk11u-2N  38589  cdlemk12u-2N  38590  cdlemk26-3  38606  cdlemk27-3  38607  cdlemkfid3N  38625  cdlemn2  38895  cdlemn10  38906  cdlemn11c  38909