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  29518  lshpkrlem5  40265  lplnexllnN  40715  4atexlemt  41204  4atex2  41228  4atex3  41232  trlval4  41339  cdlemc5  41346  cdlemc6  41347  cdlemd2  41350  cdleme0e  41368  cdleme0moN  41376  cdleme3g  41385  cdleme3h  41386  cdleme3  41388  cdleme4  41389  cdleme5  41391  cdleme9  41404  cdleme11fN  41415  cdleme11j  41418  cdleme11k  41419  cdleme11l  41420  cdleme11  41421  cdleme14  41424  cdleme15a  41425  cdleme15b  41426  cdleme15c  41427  cdleme16b  41430  cdleme16c  41431  cdleme16d  41432  cdleme16e  41433  cdleme16f  41434  cdleme17d1  41440  cdleme18c  41444  cdlemednpq  41450  cdleme19c  41456  cdleme20bN  41461  cdleme20d  41463  cdleme20f  41465  cdleme20g  41466  cdleme20h  41467  cdleme20j  41469  cdleme20l2  41472  cdleme20l  41473  cdleme20m  41474  cdleme22cN  41493  cdleme22d  41494  cdleme22e  41495  cdleme22f  41497  cdleme26fALTN  41513  cdleme26f  41514  cdleme26f2ALTN  41515  cdleme26f2  41516  cdleme27a  41518  cdleme28a  41521  cdlemefs44  41577  cdlemefs45ee  41581  cdleme32b  41593  cdleme32c  41594  cdleme32e  41596  cdleme35sn2aw  41609  cdleme37m  41613  cdleme39n  41617  cdleme40n  41619  cdleme40w  41621  cdleme42k  41635  cdlemeg47rv2  41661  cdlemeg46rjgN  41673  cdlemeg46rgv  41679  cdlemeg46req  41680  cdlemg2fv2  41751  cdlemg17h  41819  cdlemg31b0a  41846  cdlemg27b  41847  cdlemg31d  41851  cdlemg28b  41854  cdlemg28  41855  cdlemg29  41856  cdlemg33a  41857  cdlemg33b  41858  cdlemg33c  41859  cdlemg33d  41860  cdlemg33e  41861  cdlemg44a  41882  cdlemk7u-2N  42039  cdlemk11u-2N  42040  cdlemk12u-2N  42041  cdlemk26-3  42057  cdlemk27-3  42058  cdlemkfid3N  42076  cdlemn2  42346  cdlemn10  42357  cdlemn11c  42360