Theorem simp23l 1307

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

Assertion

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

Proof of Theorem simp23l

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  ax5seglem6  29081  lshpkrlem5  39702  lplnexllnN  40152  4atexlemt  40641  4atex2  40665  4atex3  40669  trlval4  40776  cdlemc5  40783  cdlemc6  40784  cdlemd2  40787  cdleme0e  40805  cdleme0moN  40813  cdleme3g  40822  cdleme3h  40823  cdleme3  40825  cdleme4  40826  cdleme5  40828  cdleme9  40841  cdleme11fN  40852  cdleme11j  40855  cdleme11k  40856  cdleme11l  40857  cdleme11  40858  cdleme14  40861  cdleme15a  40862  cdleme15b  40863  cdleme15c  40864  cdleme16b  40867  cdleme16c  40868  cdleme16d  40869  cdleme16e  40870  cdleme16f  40871  cdleme17d1  40877  cdleme18c  40881  cdlemednpq  40887  cdleme19c  40893  cdleme20bN  40898  cdleme20d  40900  cdleme20f  40902  cdleme20g  40903  cdleme20h  40904  cdleme20j  40906  cdleme20l2  40909  cdleme20l  40910  cdleme20m  40911  cdleme22cN  40930  cdleme22d  40931  cdleme22e  40932  cdleme22f  40934  cdleme26fALTN  40950  cdleme26f  40951  cdleme26f2ALTN  40952  cdleme26f2  40953  cdleme27a  40955  cdleme28a  40958  cdlemefs44  41014  cdlemefs45ee  41018  cdleme32b  41030  cdleme32c  41031  cdleme32e  41033  cdleme35sn2aw  41046  cdleme37m  41050  cdleme39n  41054  cdleme40n  41056  cdleme40w  41058  cdleme42k  41072  cdlemeg47rv2  41098  cdlemeg46rjgN  41110  cdlemeg46rgv  41116  cdlemeg46req  41117  cdlemg2fv2  41188  cdlemg17h  41256  cdlemg31b0a  41283  cdlemg27b  41284  cdlemg31d  41288  cdlemg28b  41291  cdlemg28  41292  cdlemg29  41293  cdlemg33a  41294  cdlemg33b  41295  cdlemg33c  41296  cdlemg33d  41297  cdlemg33e  41298  cdlemg44a  41319  cdlemk7u-2N  41476  cdlemk11u-2N  41477  cdlemk12u-2N  41478  cdlemk26-3  41494  cdlemk27-3  41495  cdlemkfid3N  41513  cdlemn2  41783  cdlemn10  41794  cdlemn11c  41797