Theorem simp23l 1296

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

Assertion

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

Proof of Theorem simp23l

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

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

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

This theorem is referenced by:  ax5seglem6  29017  lshpkrlem5  39574  lplnexllnN  40024  4atexlemt  40513  4atex2  40537  4atex3  40541  trlval4  40648  cdlemc5  40655  cdlemc6  40656  cdlemd2  40659  cdleme0e  40677  cdleme0moN  40685  cdleme3g  40694  cdleme3h  40695  cdleme3  40697  cdleme4  40698  cdleme5  40700  cdleme9  40713  cdleme11fN  40724  cdleme11j  40727  cdleme11k  40728  cdleme11l  40729  cdleme11  40730  cdleme14  40733  cdleme15a  40734  cdleme15b  40735  cdleme15c  40736  cdleme16b  40739  cdleme16c  40740  cdleme16d  40741  cdleme16e  40742  cdleme16f  40743  cdleme17d1  40749  cdleme18c  40753  cdlemednpq  40759  cdleme19c  40765  cdleme20bN  40770  cdleme20d  40772  cdleme20f  40774  cdleme20g  40775  cdleme20h  40776  cdleme20j  40778  cdleme20l2  40781  cdleme20l  40782  cdleme20m  40783  cdleme22cN  40802  cdleme22d  40803  cdleme22e  40804  cdleme22f  40806  cdleme26fALTN  40822  cdleme26f  40823  cdleme26f2ALTN  40824  cdleme26f2  40825  cdleme27a  40827  cdleme28a  40830  cdlemefs44  40886  cdlemefs45ee  40890  cdleme32b  40902  cdleme32c  40903  cdleme32e  40905  cdleme35sn2aw  40918  cdleme37m  40922  cdleme39n  40926  cdleme40n  40928  cdleme40w  40930  cdleme42k  40944  cdlemeg47rv2  40970  cdlemeg46rjgN  40982  cdlemeg46rgv  40988  cdlemeg46req  40989  cdlemg2fv2  41060  cdlemg17h  41128  cdlemg31b0a  41155  cdlemg27b  41156  cdlemg31d  41160  cdlemg28b  41163  cdlemg28  41164  cdlemg29  41165  cdlemg33a  41166  cdlemg33b  41167  cdlemg33c  41168  cdlemg33d  41169  cdlemg33e  41170  cdlemg44a  41191  cdlemk7u-2N  41348  cdlemk11u-2N  41349  cdlemk12u-2N  41350  cdlemk26-3  41366  cdlemk27-3  41367  cdlemkfid3N  41385  cdlemn2  41655  cdlemn10  41666  cdlemn11c  41669