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  28897  lshpkrlem5  39092  lplnexllnN  39543  4atexlemt  40032  4atex2  40056  4atex3  40060  trlval4  40167  cdlemc5  40174  cdlemc6  40175  cdlemd2  40178  cdleme0e  40196  cdleme0moN  40204  cdleme3g  40213  cdleme3h  40214  cdleme3  40216  cdleme4  40217  cdleme5  40219  cdleme9  40232  cdleme11fN  40243  cdleme11j  40246  cdleme11k  40247  cdleme11l  40248  cdleme11  40249  cdleme14  40252  cdleme15a  40253  cdleme15b  40254  cdleme15c  40255  cdleme16b  40258  cdleme16c  40259  cdleme16d  40260  cdleme16e  40261  cdleme16f  40262  cdleme17d1  40268  cdleme18c  40272  cdlemednpq  40278  cdleme19c  40284  cdleme20bN  40289  cdleme20d  40291  cdleme20f  40293  cdleme20g  40294  cdleme20h  40295  cdleme20j  40297  cdleme20l2  40300  cdleme20l  40301  cdleme20m  40302  cdleme22cN  40321  cdleme22d  40322  cdleme22e  40323  cdleme22f  40325  cdleme26fALTN  40341  cdleme26f  40342  cdleme26f2ALTN  40343  cdleme26f2  40344  cdleme27a  40346  cdleme28a  40349  cdlemefs44  40405  cdlemefs45ee  40409  cdleme32b  40421  cdleme32c  40422  cdleme32e  40424  cdleme35sn2aw  40437  cdleme37m  40441  cdleme39n  40445  cdleme40n  40447  cdleme40w  40449  cdleme42k  40463  cdlemeg47rv2  40489  cdlemeg46rjgN  40501  cdlemeg46rgv  40507  cdlemeg46req  40508  cdlemg2fv2  40579  cdlemg17h  40647  cdlemg31b0a  40674  cdlemg27b  40675  cdlemg31d  40679  cdlemg28b  40682  cdlemg28  40683  cdlemg29  40684  cdlemg33a  40685  cdlemg33b  40686  cdlemg33c  40687  cdlemg33d  40688  cdlemg33e  40689  cdlemg44a  40710  cdlemk7u-2N  40867  cdlemk11u-2N  40868  cdlemk12u-2N  40869  cdlemk26-3  40885  cdlemk27-3  40886  cdlemkfid3N  40904  cdlemn2  41174  cdlemn10  41185  cdlemn11c  41188