Theorem simp23l 1313

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

Assertion

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

Proof of Theorem simp23l

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ax5seglem6  29321  lshpkrlem5  39929  lplnexllnN  40379  4atexlemt  40868  4atex2  40892  4atex3  40896  trlval4  41003  cdlemc5  41010  cdlemc6  41011  cdlemd2  41014  cdleme0e  41032  cdleme0moN  41040  cdleme3g  41049  cdleme3h  41050  cdleme3  41052  cdleme4  41053  cdleme5  41055  cdleme9  41068  cdleme11fN  41079  cdleme11j  41082  cdleme11k  41083  cdleme11l  41084  cdleme11  41085  cdleme14  41088  cdleme15a  41089  cdleme15b  41090  cdleme15c  41091  cdleme16b  41094  cdleme16c  41095  cdleme16d  41096  cdleme16e  41097  cdleme16f  41098  cdleme17d1  41104  cdleme18c  41108  cdlemednpq  41114  cdleme19c  41120  cdleme20bN  41125  cdleme20d  41127  cdleme20f  41129  cdleme20g  41130  cdleme20h  41131  cdleme20j  41133  cdleme20l2  41136  cdleme20l  41137  cdleme20m  41138  cdleme22cN  41157  cdleme22d  41158  cdleme22e  41159  cdleme22f  41161  cdleme26fALTN  41177  cdleme26f  41178  cdleme26f2ALTN  41179  cdleme26f2  41180  cdleme27a  41182  cdleme28a  41185  cdlemefs44  41241  cdlemefs45ee  41245  cdleme32b  41257  cdleme32c  41258  cdleme32e  41260  cdleme35sn2aw  41273  cdleme37m  41277  cdleme39n  41281  cdleme40n  41283  cdleme40w  41285  cdleme42k  41299  cdlemeg47rv2  41325  cdlemeg46rjgN  41337  cdlemeg46rgv  41343  cdlemeg46req  41344  cdlemg2fv2  41415  cdlemg17h  41483  cdlemg31b0a  41510  cdlemg27b  41511  cdlemg31d  41515  cdlemg28b  41518  cdlemg28  41519  cdlemg29  41520  cdlemg33a  41521  cdlemg33b  41522  cdlemg33c  41523  cdlemg33d  41524  cdlemg33e  41525  cdlemg44a  41546  cdlemk7u-2N  41703  cdlemk11u-2N  41704  cdlemk12u-2N  41705  cdlemk26-3  41721  cdlemk27-3  41722  cdlemkfid3N  41740  cdlemn2  42010  cdlemn10  42021  cdlemn11c  42024