Theorem simp23l 1175

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

Assertion

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

Proof of Theorem simp23l

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  ax5seglem6  25614  lshpkrlem5  33419  lplnexllnN  33868  4atexlemt  34357  4atex2  34381  4atex3  34385  trlval4  34493  cdlemc5  34500  cdlemc6  34501  cdlemd2  34504  cdleme0e  34522  cdleme0moN  34530  cdleme3g  34539  cdleme3h  34540  cdleme3  34542  cdleme4  34543  cdleme5  34545  cdleme9  34558  cdleme11fN  34569  cdleme11j  34572  cdleme11k  34573  cdleme11l  34574  cdleme11  34575  cdleme14  34578  cdleme15a  34579  cdleme15b  34580  cdleme15c  34581  cdleme16b  34584  cdleme16c  34585  cdleme16d  34586  cdleme16e  34587  cdleme16f  34588  cdleme17d1  34594  cdleme18c  34598  cdlemednpq  34604  cdleme19c  34611  cdleme20bN  34616  cdleme20d  34618  cdleme20f  34620  cdleme20g  34621  cdleme20h  34622  cdleme20j  34624  cdleme20l2  34627  cdleme20l  34628  cdleme20m  34629  cdleme22cN  34648  cdleme22d  34649  cdleme22e  34650  cdleme22f  34652  cdleme26fALTN  34668  cdleme26f  34669  cdleme26f2ALTN  34670  cdleme26f2  34671  cdleme27a  34673  cdleme28a  34676  cdlemefs44  34732  cdlemefs45ee  34736  cdleme32b  34748  cdleme32c  34749  cdleme32e  34751  cdleme35sn2aw  34764  cdleme37m  34768  cdleme39n  34772  cdleme40n  34774  cdleme40w  34776  cdleme42k  34790  cdlemeg47rv2  34816  cdlemeg46rjgN  34828  cdlemeg46rgv  34834  cdlemeg46req  34835  cdlemg2fv2  34906  cdlemg17h  34974  cdlemg31b0a  35001  cdlemg27b  35002  cdlemg31d  35006  cdlemg28b  35009  cdlemg28  35010  cdlemg29  35011  cdlemg33a  35012  cdlemg33b  35013  cdlemg33c  35014  cdlemg33d  35015  cdlemg33e  35016  cdlemg44a  35037  cdlemk7u-2N  35194  cdlemk11u-2N  35195  cdlemk12u-2N  35196  cdlemk26-3  35212  cdlemk27-3  35213  cdlemkfid3N  35231  cdlemn2  35502  cdlemn10  35513  cdlemn11c  35516