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 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  ax5seglem6  29265  lshpkrlem5  39869  lplnexllnN  40319  4atexlemt  40808  4atex2  40832  4atex3  40836  trlval4  40943  cdlemc5  40950  cdlemc6  40951  cdlemd2  40954  cdleme0e  40972  cdleme0moN  40980  cdleme3g  40989  cdleme3h  40990  cdleme3  40992  cdleme4  40993  cdleme5  40995  cdleme9  41008  cdleme11fN  41019  cdleme11j  41022  cdleme11k  41023  cdleme11l  41024  cdleme11  41025  cdleme14  41028  cdleme15a  41029  cdleme15b  41030  cdleme15c  41031  cdleme16b  41034  cdleme16c  41035  cdleme16d  41036  cdleme16e  41037  cdleme16f  41038  cdleme17d1  41044  cdleme18c  41048  cdlemednpq  41054  cdleme19c  41060  cdleme20bN  41065  cdleme20d  41067  cdleme20f  41069  cdleme20g  41070  cdleme20h  41071  cdleme20j  41073  cdleme20l2  41076  cdleme20l  41077  cdleme20m  41078  cdleme22cN  41097  cdleme22d  41098  cdleme22e  41099  cdleme22f  41101  cdleme26fALTN  41117  cdleme26f  41118  cdleme26f2ALTN  41119  cdleme26f2  41120  cdleme27a  41122  cdleme28a  41125  cdlemefs44  41181  cdlemefs45ee  41185  cdleme32b  41197  cdleme32c  41198  cdleme32e  41200  cdleme35sn2aw  41213  cdleme37m  41217  cdleme39n  41221  cdleme40n  41223  cdleme40w  41225  cdleme42k  41239  cdlemeg47rv2  41265  cdlemeg46rjgN  41277  cdlemeg46rgv  41283  cdlemeg46req  41284  cdlemg2fv2  41355  cdlemg17h  41423  cdlemg31b0a  41450  cdlemg27b  41451  cdlemg31d  41455  cdlemg28b  41458  cdlemg28  41459  cdlemg29  41460  cdlemg33a  41461  cdlemg33b  41462  cdlemg33c  41463  cdlemg33d  41464  cdlemg33e  41465  cdlemg44a  41486  cdlemk7u-2N  41643  cdlemk11u-2N  41644  cdlemk12u-2N  41645  cdlemk26-3  41661  cdlemk27-3  41662  cdlemkfid3N  41680  cdlemn2  41950  cdlemn10  41961  cdlemn11c  41964