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  28861  lshpkrlem5  39107  lplnexllnN  39558  4atexlemt  40047  4atex2  40071  4atex3  40075  trlval4  40182  cdlemc5  40189  cdlemc6  40190  cdlemd2  40193  cdleme0e  40211  cdleme0moN  40219  cdleme3g  40228  cdleme3h  40229  cdleme3  40231  cdleme4  40232  cdleme5  40234  cdleme9  40247  cdleme11fN  40258  cdleme11j  40261  cdleme11k  40262  cdleme11l  40263  cdleme11  40264  cdleme14  40267  cdleme15a  40268  cdleme15b  40269  cdleme15c  40270  cdleme16b  40273  cdleme16c  40274  cdleme16d  40275  cdleme16e  40276  cdleme16f  40277  cdleme17d1  40283  cdleme18c  40287  cdlemednpq  40293  cdleme19c  40299  cdleme20bN  40304  cdleme20d  40306  cdleme20f  40308  cdleme20g  40309  cdleme20h  40310  cdleme20j  40312  cdleme20l2  40315  cdleme20l  40316  cdleme20m  40317  cdleme22cN  40336  cdleme22d  40337  cdleme22e  40338  cdleme22f  40340  cdleme26fALTN  40356  cdleme26f  40357  cdleme26f2ALTN  40358  cdleme26f2  40359  cdleme27a  40361  cdleme28a  40364  cdlemefs44  40420  cdlemefs45ee  40424  cdleme32b  40436  cdleme32c  40437  cdleme32e  40439  cdleme35sn2aw  40452  cdleme37m  40456  cdleme39n  40460  cdleme40n  40462  cdleme40w  40464  cdleme42k  40478  cdlemeg47rv2  40504  cdlemeg46rjgN  40516  cdlemeg46rgv  40522  cdlemeg46req  40523  cdlemg2fv2  40594  cdlemg17h  40662  cdlemg31b0a  40689  cdlemg27b  40690  cdlemg31d  40694  cdlemg28b  40697  cdlemg28  40698  cdlemg29  40699  cdlemg33a  40700  cdlemg33b  40701  cdlemg33c  40702  cdlemg33d  40703  cdlemg33e  40704  cdlemg44a  40725  cdlemk7u-2N  40882  cdlemk11u-2N  40883  cdlemk12u-2N  40884  cdlemk26-3  40900  cdlemk27-3  40901  cdlemkfid3N  40919  cdlemn2  41189  cdlemn10  41200  cdlemn11c  41203