Theorem simp23l 1378

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

Assertion

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

Proof of Theorem simp23l

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071

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 197  df-an 383  df-3an 1073

This theorem is referenced by:  ax5seglem6  26028  lshpkrlem5  34916  lplnexllnN  35365  4atexlemt  35854  4atex2  35878  4atex3  35882  trlval4  35990  cdlemc5  35997  cdlemc6  35998  cdlemd2  36001  cdleme0e  36019  cdleme0moN  36027  cdleme3g  36036  cdleme3h  36037  cdleme3  36039  cdleme4  36040  cdleme5  36042  cdleme9  36055  cdleme11fN  36066  cdleme11j  36069  cdleme11k  36070  cdleme11l  36071  cdleme11  36072  cdleme14  36075  cdleme15a  36076  cdleme15b  36077  cdleme15c  36078  cdleme16b  36081  cdleme16c  36082  cdleme16d  36083  cdleme16e  36084  cdleme16f  36085  cdleme17d1  36091  cdleme18c  36095  cdlemednpq  36101  cdleme19c  36107  cdleme20bN  36112  cdleme20d  36114  cdleme20f  36116  cdleme20g  36117  cdleme20h  36118  cdleme20j  36120  cdleme20l2  36123  cdleme20l  36124  cdleme20m  36125  cdleme22cN  36144  cdleme22d  36145  cdleme22e  36146  cdleme22f  36148  cdleme26fALTN  36164  cdleme26f  36165  cdleme26f2ALTN  36166  cdleme26f2  36167  cdleme27a  36169  cdleme28a  36172  cdlemefs44  36228  cdlemefs45ee  36232  cdleme32b  36244  cdleme32c  36245  cdleme32e  36247  cdleme35sn2aw  36260  cdleme37m  36264  cdleme39n  36268  cdleme40n  36270  cdleme40w  36272  cdleme42k  36286  cdlemeg47rv2  36312  cdlemeg46rjgN  36324  cdlemeg46rgv  36330  cdlemeg46req  36331  cdlemg2fv2  36402  cdlemg17h  36470  cdlemg31b0a  36497  cdlemg27b  36498  cdlemg31d  36502  cdlemg28b  36505  cdlemg28  36506  cdlemg29  36507  cdlemg33a  36508  cdlemg33b  36509  cdlemg33c  36510  cdlemg33d  36511  cdlemg33e  36512  cdlemg44a  36533  cdlemk7u-2N  36690  cdlemk11u-2N  36691  cdlemk12u-2N  36692  cdlemk26-3  36708  cdlemk27-3  36709  cdlemkfid3N  36727  cdlemn2  36998  cdlemn10  37009  cdlemn11c  37012