Theorem simp23l 1290

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

Assertion

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

Proof of Theorem simp23l

Step	Hyp	Ref	Expression
1		simp3l 1197	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant2 1130	1 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  ax5seglem6  26722  lshpkrlem5  36252  lplnexllnN  36702  4atexlemt  37191  4atex2  37215  4atex3  37219  trlval4  37326  cdlemc5  37333  cdlemc6  37334  cdlemd2  37337  cdleme0e  37355  cdleme0moN  37363  cdleme3g  37372  cdleme3h  37373  cdleme3  37375  cdleme4  37376  cdleme5  37378  cdleme9  37391  cdleme11fN  37402  cdleme11j  37405  cdleme11k  37406  cdleme11l  37407  cdleme11  37408  cdleme14  37411  cdleme15a  37412  cdleme15b  37413  cdleme15c  37414  cdleme16b  37417  cdleme16c  37418  cdleme16d  37419  cdleme16e  37420  cdleme16f  37421  cdleme17d1  37427  cdleme18c  37431  cdlemednpq  37437  cdleme19c  37443  cdleme20bN  37448  cdleme20d  37450  cdleme20f  37452  cdleme20g  37453  cdleme20h  37454  cdleme20j  37456  cdleme20l2  37459  cdleme20l  37460  cdleme20m  37461  cdleme22cN  37480  cdleme22d  37481  cdleme22e  37482  cdleme22f  37484  cdleme26fALTN  37500  cdleme26f  37501  cdleme26f2ALTN  37502  cdleme26f2  37503  cdleme27a  37505  cdleme28a  37508  cdlemefs44  37564  cdlemefs45ee  37568  cdleme32b  37580  cdleme32c  37581  cdleme32e  37583  cdleme35sn2aw  37596  cdleme37m  37600  cdleme39n  37604  cdleme40n  37606  cdleme40w  37608  cdleme42k  37622  cdlemeg47rv2  37648  cdlemeg46rjgN  37660  cdlemeg46rgv  37666  cdlemeg46req  37667  cdlemg2fv2  37738  cdlemg17h  37806  cdlemg31b0a  37833  cdlemg27b  37834  cdlemg31d  37838  cdlemg28b  37841  cdlemg28  37842  cdlemg29  37843  cdlemg33a  37844  cdlemg33b  37845  cdlemg33c  37846  cdlemg33d  37847  cdlemg33e  37848  cdlemg44a  37869  cdlemk7u-2N  38026  cdlemk11u-2N  38027  cdlemk12u-2N  38028  cdlemk26-3  38044  cdlemk27-3  38045  cdlemkfid3N  38063  cdlemn2  38333  cdlemn10  38344  cdlemn11c  38347