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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  ax5seglem6  28192  lshpkrlem5  37984  lplnexllnN  38435  4atexlemt  38924  4atex2  38948  4atex3  38952  trlval4  39059  cdlemc5  39066  cdlemc6  39067  cdlemd2  39070  cdleme0e  39088  cdleme0moN  39096  cdleme3g  39105  cdleme3h  39106  cdleme3  39108  cdleme4  39109  cdleme5  39111  cdleme9  39124  cdleme11fN  39135  cdleme11j  39138  cdleme11k  39139  cdleme11l  39140  cdleme11  39141  cdleme14  39144  cdleme15a  39145  cdleme15b  39146  cdleme15c  39147  cdleme16b  39150  cdleme16c  39151  cdleme16d  39152  cdleme16e  39153  cdleme16f  39154  cdleme17d1  39160  cdleme18c  39164  cdlemednpq  39170  cdleme19c  39176  cdleme20bN  39181  cdleme20d  39183  cdleme20f  39185  cdleme20g  39186  cdleme20h  39187  cdleme20j  39189  cdleme20l2  39192  cdleme20l  39193  cdleme20m  39194  cdleme22cN  39213  cdleme22d  39214  cdleme22e  39215  cdleme22f  39217  cdleme26fALTN  39233  cdleme26f  39234  cdleme26f2ALTN  39235  cdleme26f2  39236  cdleme27a  39238  cdleme28a  39241  cdlemefs44  39297  cdlemefs45ee  39301  cdleme32b  39313  cdleme32c  39314  cdleme32e  39316  cdleme35sn2aw  39329  cdleme37m  39333  cdleme39n  39337  cdleme40n  39339  cdleme40w  39341  cdleme42k  39355  cdlemeg47rv2  39381  cdlemeg46rjgN  39393  cdlemeg46rgv  39399  cdlemeg46req  39400  cdlemg2fv2  39471  cdlemg17h  39539  cdlemg31b0a  39566  cdlemg27b  39567  cdlemg31d  39571  cdlemg28b  39574  cdlemg28  39575  cdlemg29  39576  cdlemg33a  39577  cdlemg33b  39578  cdlemg33c  39579  cdlemg33d  39580  cdlemg33e  39581  cdlemg44a  39602  cdlemk7u-2N  39759  cdlemk11u-2N  39760  cdlemk12u-2N  39761  cdlemk26-3  39777  cdlemk27-3  39778  cdlemkfid3N  39796  cdlemn2  40066  cdlemn10  40077  cdlemn11c  40080