Theorem simp23l 1295

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

Assertion

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

Proof of Theorem simp23l

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  ax5seglem6  28910  lshpkrlem5  39152  lplnexllnN  39602  4atexlemt  40091  4atex2  40115  4atex3  40119  trlval4  40226  cdlemc5  40233  cdlemc6  40234  cdlemd2  40237  cdleme0e  40255  cdleme0moN  40263  cdleme3g  40272  cdleme3h  40273  cdleme3  40275  cdleme4  40276  cdleme5  40278  cdleme9  40291  cdleme11fN  40302  cdleme11j  40305  cdleme11k  40306  cdleme11l  40307  cdleme11  40308  cdleme14  40311  cdleme15a  40312  cdleme15b  40313  cdleme15c  40314  cdleme16b  40317  cdleme16c  40318  cdleme16d  40319  cdleme16e  40320  cdleme16f  40321  cdleme17d1  40327  cdleme18c  40331  cdlemednpq  40337  cdleme19c  40343  cdleme20bN  40348  cdleme20d  40350  cdleme20f  40352  cdleme20g  40353  cdleme20h  40354  cdleme20j  40356  cdleme20l2  40359  cdleme20l  40360  cdleme20m  40361  cdleme22cN  40380  cdleme22d  40381  cdleme22e  40382  cdleme22f  40384  cdleme26fALTN  40400  cdleme26f  40401  cdleme26f2ALTN  40402  cdleme26f2  40403  cdleme27a  40405  cdleme28a  40408  cdlemefs44  40464  cdlemefs45ee  40468  cdleme32b  40480  cdleme32c  40481  cdleme32e  40483  cdleme35sn2aw  40496  cdleme37m  40500  cdleme39n  40504  cdleme40n  40506  cdleme40w  40508  cdleme42k  40522  cdlemeg47rv2  40548  cdlemeg46rjgN  40560  cdlemeg46rgv  40566  cdlemeg46req  40567  cdlemg2fv2  40638  cdlemg17h  40706  cdlemg31b0a  40733  cdlemg27b  40734  cdlemg31d  40738  cdlemg28b  40741  cdlemg28  40742  cdlemg29  40743  cdlemg33a  40744  cdlemg33b  40745  cdlemg33c  40746  cdlemg33d  40747  cdlemg33e  40748  cdlemg44a  40769  cdlemk7u-2N  40926  cdlemk11u-2N  40927  cdlemk12u-2N  40928  cdlemk26-3  40944  cdlemk27-3  40945  cdlemkfid3N  40963  cdlemn2  41233  cdlemn10  41244  cdlemn11c  41247