Theorem simp23l 1292

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

Assertion

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

Proof of Theorem simp23l

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  ax5seglem6  27205  lshpkrlem5  37055  lplnexllnN  37505  4atexlemt  37994  4atex2  38018  4atex3  38022  trlval4  38129  cdlemc5  38136  cdlemc6  38137  cdlemd2  38140  cdleme0e  38158  cdleme0moN  38166  cdleme3g  38175  cdleme3h  38176  cdleme3  38178  cdleme4  38179  cdleme5  38181  cdleme9  38194  cdleme11fN  38205  cdleme11j  38208  cdleme11k  38209  cdleme11l  38210  cdleme11  38211  cdleme14  38214  cdleme15a  38215  cdleme15b  38216  cdleme15c  38217  cdleme16b  38220  cdleme16c  38221  cdleme16d  38222  cdleme16e  38223  cdleme16f  38224  cdleme17d1  38230  cdleme18c  38234  cdlemednpq  38240  cdleme19c  38246  cdleme20bN  38251  cdleme20d  38253  cdleme20f  38255  cdleme20g  38256  cdleme20h  38257  cdleme20j  38259  cdleme20l2  38262  cdleme20l  38263  cdleme20m  38264  cdleme22cN  38283  cdleme22d  38284  cdleme22e  38285  cdleme22f  38287  cdleme26fALTN  38303  cdleme26f  38304  cdleme26f2ALTN  38305  cdleme26f2  38306  cdleme27a  38308  cdleme28a  38311  cdlemefs44  38367  cdlemefs45ee  38371  cdleme32b  38383  cdleme32c  38384  cdleme32e  38386  cdleme35sn2aw  38399  cdleme37m  38403  cdleme39n  38407  cdleme40n  38409  cdleme40w  38411  cdleme42k  38425  cdlemeg47rv2  38451  cdlemeg46rjgN  38463  cdlemeg46rgv  38469  cdlemeg46req  38470  cdlemg2fv2  38541  cdlemg17h  38609  cdlemg31b0a  38636  cdlemg27b  38637  cdlemg31d  38641  cdlemg28b  38644  cdlemg28  38645  cdlemg29  38646  cdlemg33a  38647  cdlemg33b  38648  cdlemg33c  38649  cdlemg33d  38650  cdlemg33e  38651  cdlemg44a  38672  cdlemk7u-2N  38829  cdlemk11u-2N  38830  cdlemk12u-2N  38831  cdlemk26-3  38847  cdlemk27-3  38848  cdlemkfid3N  38866  cdlemn2  39136  cdlemn10  39147  cdlemn11c  39150