Theorem simp23l 1302

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

Assertion

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

Proof of Theorem simp23l

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

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

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 209  df-an 398  df-3an 1095

This theorem is referenced by:  ax5seglem6  29023  lshpkrlem5  39619  lplnexllnN  40069  4atexlemt  40558  4atex2  40582  4atex3  40586  trlval4  40693  cdlemc5  40700  cdlemc6  40701  cdlemd2  40704  cdleme0e  40722  cdleme0moN  40730  cdleme3g  40739  cdleme3h  40740  cdleme3  40742  cdleme4  40743  cdleme5  40745  cdleme9  40758  cdleme11fN  40769  cdleme11j  40772  cdleme11k  40773  cdleme11l  40774  cdleme11  40775  cdleme14  40778  cdleme15a  40779  cdleme15b  40780  cdleme15c  40781  cdleme16b  40784  cdleme16c  40785  cdleme16d  40786  cdleme16e  40787  cdleme16f  40788  cdleme17d1  40794  cdleme18c  40798  cdlemednpq  40804  cdleme19c  40810  cdleme20bN  40815  cdleme20d  40817  cdleme20f  40819  cdleme20g  40820  cdleme20h  40821  cdleme20j  40823  cdleme20l2  40826  cdleme20l  40827  cdleme20m  40828  cdleme22cN  40847  cdleme22d  40848  cdleme22e  40849  cdleme22f  40851  cdleme26fALTN  40867  cdleme26f  40868  cdleme26f2ALTN  40869  cdleme26f2  40870  cdleme27a  40872  cdleme28a  40875  cdlemefs44  40931  cdlemefs45ee  40935  cdleme32b  40947  cdleme32c  40948  cdleme32e  40950  cdleme35sn2aw  40963  cdleme37m  40967  cdleme39n  40971  cdleme40n  40973  cdleme40w  40975  cdleme42k  40989  cdlemeg47rv2  41015  cdlemeg46rjgN  41027  cdlemeg46rgv  41033  cdlemeg46req  41034  cdlemg2fv2  41105  cdlemg17h  41173  cdlemg31b0a  41200  cdlemg27b  41201  cdlemg31d  41205  cdlemg28b  41208  cdlemg28  41209  cdlemg29  41210  cdlemg33a  41211  cdlemg33b  41212  cdlemg33c  41213  cdlemg33d  41214  cdlemg33e  41215  cdlemg44a  41236  cdlemk7u-2N  41393  cdlemk11u-2N  41394  cdlemk12u-2N  41395  cdlemk26-3  41411  cdlemk27-3  41412  cdlemkfid3N  41430  cdlemn2  41700  cdlemn10  41711  cdlemn11c  41714