Theorem simp23l 1291

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

Assertion

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

Proof of Theorem simp23l

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  ax5seglem6  28837  lshpkrlem5  38736  lplnexllnN  39187  4atexlemt  39676  4atex2  39700  4atex3  39704  trlval4  39811  cdlemc5  39818  cdlemc6  39819  cdlemd2  39822  cdleme0e  39840  cdleme0moN  39848  cdleme3g  39857  cdleme3h  39858  cdleme3  39860  cdleme4  39861  cdleme5  39863  cdleme9  39876  cdleme11fN  39887  cdleme11j  39890  cdleme11k  39891  cdleme11l  39892  cdleme11  39893  cdleme14  39896  cdleme15a  39897  cdleme15b  39898  cdleme15c  39899  cdleme16b  39902  cdleme16c  39903  cdleme16d  39904  cdleme16e  39905  cdleme16f  39906  cdleme17d1  39912  cdleme18c  39916  cdlemednpq  39922  cdleme19c  39928  cdleme20bN  39933  cdleme20d  39935  cdleme20f  39937  cdleme20g  39938  cdleme20h  39939  cdleme20j  39941  cdleme20l2  39944  cdleme20l  39945  cdleme20m  39946  cdleme22cN  39965  cdleme22d  39966  cdleme22e  39967  cdleme22f  39969  cdleme26fALTN  39985  cdleme26f  39986  cdleme26f2ALTN  39987  cdleme26f2  39988  cdleme27a  39990  cdleme28a  39993  cdlemefs44  40049  cdlemefs45ee  40053  cdleme32b  40065  cdleme32c  40066  cdleme32e  40068  cdleme35sn2aw  40081  cdleme37m  40085  cdleme39n  40089  cdleme40n  40091  cdleme40w  40093  cdleme42k  40107  cdlemeg47rv2  40133  cdlemeg46rjgN  40145  cdlemeg46rgv  40151  cdlemeg46req  40152  cdlemg2fv2  40223  cdlemg17h  40291  cdlemg31b0a  40318  cdlemg27b  40319  cdlemg31d  40323  cdlemg28b  40326  cdlemg28  40327  cdlemg29  40328  cdlemg33a  40329  cdlemg33b  40330  cdlemg33c  40331  cdlemg33d  40332  cdlemg33e  40333  cdlemg44a  40354  cdlemk7u-2N  40511  cdlemk11u-2N  40512  cdlemk12u-2N  40513  cdlemk26-3  40529  cdlemk27-3  40530  cdlemkfid3N  40548  cdlemn2  40818  cdlemn10  40829  cdlemn11c  40832