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  29003  lshpkrlem5  39560  lplnexllnN  40010  4atexlemt  40499  4atex2  40523  4atex3  40527  trlval4  40634  cdlemc5  40641  cdlemc6  40642  cdlemd2  40645  cdleme0e  40663  cdleme0moN  40671  cdleme3g  40680  cdleme3h  40681  cdleme3  40683  cdleme4  40684  cdleme5  40686  cdleme9  40699  cdleme11fN  40710  cdleme11j  40713  cdleme11k  40714  cdleme11l  40715  cdleme11  40716  cdleme14  40719  cdleme15a  40720  cdleme15b  40721  cdleme15c  40722  cdleme16b  40725  cdleme16c  40726  cdleme16d  40727  cdleme16e  40728  cdleme16f  40729  cdleme17d1  40735  cdleme18c  40739  cdlemednpq  40745  cdleme19c  40751  cdleme20bN  40756  cdleme20d  40758  cdleme20f  40760  cdleme20g  40761  cdleme20h  40762  cdleme20j  40764  cdleme20l2  40767  cdleme20l  40768  cdleme20m  40769  cdleme22cN  40788  cdleme22d  40789  cdleme22e  40790  cdleme22f  40792  cdleme26fALTN  40808  cdleme26f  40809  cdleme26f2ALTN  40810  cdleme26f2  40811  cdleme27a  40813  cdleme28a  40816  cdlemefs44  40872  cdlemefs45ee  40876  cdleme32b  40888  cdleme32c  40889  cdleme32e  40891  cdleme35sn2aw  40904  cdleme37m  40908  cdleme39n  40912  cdleme40n  40914  cdleme40w  40916  cdleme42k  40930  cdlemeg47rv2  40956  cdlemeg46rjgN  40968  cdlemeg46rgv  40974  cdlemeg46req  40975  cdlemg2fv2  41046  cdlemg17h  41114  cdlemg31b0a  41141  cdlemg27b  41142  cdlemg31d  41146  cdlemg28b  41149  cdlemg28  41150  cdlemg29  41151  cdlemg33a  41152  cdlemg33b  41153  cdlemg33c  41154  cdlemg33d  41155  cdlemg33e  41156  cdlemg44a  41177  cdlemk7u-2N  41334  cdlemk11u-2N  41335  cdlemk12u-2N  41336  cdlemk26-3  41352  cdlemk27-3  41353  cdlemkfid3N  41371  cdlemn2  41641  cdlemn10  41652  cdlemn11c  41655