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  28879  lshpkrlem5  39103  lplnexllnN  39553  4atexlemt  40042  4atex2  40066  4atex3  40070  trlval4  40177  cdlemc5  40184  cdlemc6  40185  cdlemd2  40188  cdleme0e  40206  cdleme0moN  40214  cdleme3g  40223  cdleme3h  40224  cdleme3  40226  cdleme4  40227  cdleme5  40229  cdleme9  40242  cdleme11fN  40253  cdleme11j  40256  cdleme11k  40257  cdleme11l  40258  cdleme11  40259  cdleme14  40262  cdleme15a  40263  cdleme15b  40264  cdleme15c  40265  cdleme16b  40268  cdleme16c  40269  cdleme16d  40270  cdleme16e  40271  cdleme16f  40272  cdleme17d1  40278  cdleme18c  40282  cdlemednpq  40288  cdleme19c  40294  cdleme20bN  40299  cdleme20d  40301  cdleme20f  40303  cdleme20g  40304  cdleme20h  40305  cdleme20j  40307  cdleme20l2  40310  cdleme20l  40311  cdleme20m  40312  cdleme22cN  40331  cdleme22d  40332  cdleme22e  40333  cdleme22f  40335  cdleme26fALTN  40351  cdleme26f  40352  cdleme26f2ALTN  40353  cdleme26f2  40354  cdleme27a  40356  cdleme28a  40359  cdlemefs44  40415  cdlemefs45ee  40419  cdleme32b  40431  cdleme32c  40432  cdleme32e  40434  cdleme35sn2aw  40447  cdleme37m  40451  cdleme39n  40455  cdleme40n  40457  cdleme40w  40459  cdleme42k  40473  cdlemeg47rv2  40499  cdlemeg46rjgN  40511  cdlemeg46rgv  40517  cdlemeg46req  40518  cdlemg2fv2  40589  cdlemg17h  40657  cdlemg31b0a  40684  cdlemg27b  40685  cdlemg31d  40689  cdlemg28b  40692  cdlemg28  40693  cdlemg29  40694  cdlemg33a  40695  cdlemg33b  40696  cdlemg33c  40697  cdlemg33d  40698  cdlemg33e  40699  cdlemg44a  40720  cdlemk7u-2N  40877  cdlemk11u-2N  40878  cdlemk12u-2N  40879  cdlemk26-3  40895  cdlemk27-3  40896  cdlemkfid3N  40914  cdlemn2  41184  cdlemn10  41195  cdlemn11c  41198