Theorem simp23l 1313

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

Assertion

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

Proof of Theorem simp23l

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ax5seglem6  29494  lshpkrlem5  40139  lplnexllnN  40589  4atexlemt  41078  4atex2  41102  4atex3  41106  trlval4  41213  cdlemc5  41220  cdlemc6  41221  cdlemd2  41224  cdleme0e  41242  cdleme0moN  41250  cdleme3g  41259  cdleme3h  41260  cdleme3  41262  cdleme4  41263  cdleme5  41265  cdleme9  41278  cdleme11fN  41289  cdleme11j  41292  cdleme11k  41293  cdleme11l  41294  cdleme11  41295  cdleme14  41298  cdleme15a  41299  cdleme15b  41300  cdleme15c  41301  cdleme16b  41304  cdleme16c  41305  cdleme16d  41306  cdleme16e  41307  cdleme16f  41308  cdleme17d1  41314  cdleme18c  41318  cdlemednpq  41324  cdleme19c  41330  cdleme20bN  41335  cdleme20d  41337  cdleme20f  41339  cdleme20g  41340  cdleme20h  41341  cdleme20j  41343  cdleme20l2  41346  cdleme20l  41347  cdleme20m  41348  cdleme22cN  41367  cdleme22d  41368  cdleme22e  41369  cdleme22f  41371  cdleme26fALTN  41387  cdleme26f  41388  cdleme26f2ALTN  41389  cdleme26f2  41390  cdleme27a  41392  cdleme28a  41395  cdlemefs44  41451  cdlemefs45ee  41455  cdleme32b  41467  cdleme32c  41468  cdleme32e  41470  cdleme35sn2aw  41483  cdleme37m  41487  cdleme39n  41491  cdleme40n  41493  cdleme40w  41495  cdleme42k  41509  cdlemeg47rv2  41535  cdlemeg46rjgN  41547  cdlemeg46rgv  41553  cdlemeg46req  41554  cdlemg2fv2  41625  cdlemg17h  41693  cdlemg31b0a  41720  cdlemg27b  41721  cdlemg31d  41725  cdlemg28b  41728  cdlemg28  41729  cdlemg29  41730  cdlemg33a  41731  cdlemg33b  41732  cdlemg33c  41733  cdlemg33d  41734  cdlemg33e  41735  cdlemg44a  41756  cdlemk7u-2N  41913  cdlemk11u-2N  41914  cdlemk12u-2N  41915  cdlemk26-3  41931  cdlemk27-3  41932  cdlemkfid3N  41950  cdlemn2  42220  cdlemn10  42231  cdlemn11c  42234