Theorem simp23l 1386

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

Assertion

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

Proof of Theorem simp23l

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  ax5seglem6  26051  lshpkrlem5  34913  lplnexllnN  35363  4atexlemt  35852  4atex2  35876  4atex3  35880  trlval4  35987  cdlemc5  35994  cdlemc6  35995  cdlemd2  35998  cdleme0e  36016  cdleme0moN  36024  cdleme3g  36033  cdleme3h  36034  cdleme3  36036  cdleme4  36037  cdleme5  36039  cdleme9  36052  cdleme11fN  36063  cdleme11j  36066  cdleme11k  36067  cdleme11l  36068  cdleme11  36069  cdleme14  36072  cdleme15a  36073  cdleme15b  36074  cdleme15c  36075  cdleme16b  36078  cdleme16c  36079  cdleme16d  36080  cdleme16e  36081  cdleme16f  36082  cdleme17d1  36088  cdleme18c  36092  cdlemednpq  36098  cdleme19c  36104  cdleme20bN  36109  cdleme20d  36111  cdleme20f  36113  cdleme20g  36114  cdleme20h  36115  cdleme20j  36117  cdleme20l2  36120  cdleme20l  36121  cdleme20m  36122  cdleme22cN  36141  cdleme22d  36142  cdleme22e  36143  cdleme22f  36145  cdleme26fALTN  36161  cdleme26f  36162  cdleme26f2ALTN  36163  cdleme26f2  36164  cdleme27a  36166  cdleme28a  36169  cdlemefs44  36225  cdlemefs45ee  36229  cdleme32b  36241  cdleme32c  36242  cdleme32e  36244  cdleme35sn2aw  36257  cdleme37m  36261  cdleme39n  36265  cdleme40n  36267  cdleme40w  36269  cdleme42k  36283  cdlemeg47rv2  36309  cdlemeg46rjgN  36321  cdlemeg46rgv  36327  cdlemeg46req  36328  cdlemg2fv2  36399  cdlemg17h  36467  cdlemg31b0a  36494  cdlemg27b  36495  cdlemg31d  36499  cdlemg28b  36502  cdlemg28  36503  cdlemg29  36504  cdlemg33a  36505  cdlemg33b  36506  cdlemg33c  36507  cdlemg33d  36508  cdlemg33e  36509  cdlemg44a  36530  cdlemk7u-2N  36687  cdlemk11u-2N  36688  cdlemk12u-2N  36689  cdlemk26-3  36705  cdlemk27-3  36706  cdlemkfid3N  36724  cdlemn2  36994  cdlemn10  37005  cdlemn11c  37008