Theorem simp23l 1301

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

Assertion

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

Proof of Theorem simp23l

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  ax5seglem6  29028  lshpkrlem5  39613  lplnexllnN  40063  4atexlemt  40552  4atex2  40576  4atex3  40580  trlval4  40687  cdlemc5  40694  cdlemc6  40695  cdlemd2  40698  cdleme0e  40716  cdleme0moN  40724  cdleme3g  40733  cdleme3h  40734  cdleme3  40736  cdleme4  40737  cdleme5  40739  cdleme9  40752  cdleme11fN  40763  cdleme11j  40766  cdleme11k  40767  cdleme11l  40768  cdleme11  40769  cdleme14  40772  cdleme15a  40773  cdleme15b  40774  cdleme15c  40775  cdleme16b  40778  cdleme16c  40779  cdleme16d  40780  cdleme16e  40781  cdleme16f  40782  cdleme17d1  40788  cdleme18c  40792  cdlemednpq  40798  cdleme19c  40804  cdleme20bN  40809  cdleme20d  40811  cdleme20f  40813  cdleme20g  40814  cdleme20h  40815  cdleme20j  40817  cdleme20l2  40820  cdleme20l  40821  cdleme20m  40822  cdleme22cN  40841  cdleme22d  40842  cdleme22e  40843  cdleme22f  40845  cdleme26fALTN  40861  cdleme26f  40862  cdleme26f2ALTN  40863  cdleme26f2  40864  cdleme27a  40866  cdleme28a  40869  cdlemefs44  40925  cdlemefs45ee  40929  cdleme32b  40941  cdleme32c  40942  cdleme32e  40944  cdleme35sn2aw  40957  cdleme37m  40961  cdleme39n  40965  cdleme40n  40967  cdleme40w  40969  cdleme42k  40983  cdlemeg47rv2  41009  cdlemeg46rjgN  41021  cdlemeg46rgv  41027  cdlemeg46req  41028  cdlemg2fv2  41099  cdlemg17h  41167  cdlemg31b0a  41194  cdlemg27b  41195  cdlemg31d  41199  cdlemg28b  41202  cdlemg28  41203  cdlemg29  41204  cdlemg33a  41205  cdlemg33b  41206  cdlemg33c  41207  cdlemg33d  41208  cdlemg33e  41209  cdlemg44a  41230  cdlemk7u-2N  41387  cdlemk11u-2N  41388  cdlemk12u-2N  41389  cdlemk26-3  41405  cdlemk27-3  41406  cdlemkfid3N  41424  cdlemn2  41694  cdlemn10  41705  cdlemn11c  41708