Theorem simp23l 1293

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

Assertion

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

Proof of Theorem simp23l

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

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

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 1088

This theorem is referenced by:  ax5seglem6  28963  lshpkrlem5  39095  lplnexllnN  39546  4atexlemt  40035  4atex2  40059  4atex3  40063  trlval4  40170  cdlemc5  40177  cdlemc6  40178  cdlemd2  40181  cdleme0e  40199  cdleme0moN  40207  cdleme3g  40216  cdleme3h  40217  cdleme3  40219  cdleme4  40220  cdleme5  40222  cdleme9  40235  cdleme11fN  40246  cdleme11j  40249  cdleme11k  40250  cdleme11l  40251  cdleme11  40252  cdleme14  40255  cdleme15a  40256  cdleme15b  40257  cdleme15c  40258  cdleme16b  40261  cdleme16c  40262  cdleme16d  40263  cdleme16e  40264  cdleme16f  40265  cdleme17d1  40271  cdleme18c  40275  cdlemednpq  40281  cdleme19c  40287  cdleme20bN  40292  cdleme20d  40294  cdleme20f  40296  cdleme20g  40297  cdleme20h  40298  cdleme20j  40300  cdleme20l2  40303  cdleme20l  40304  cdleme20m  40305  cdleme22cN  40324  cdleme22d  40325  cdleme22e  40326  cdleme22f  40328  cdleme26fALTN  40344  cdleme26f  40345  cdleme26f2ALTN  40346  cdleme26f2  40347  cdleme27a  40349  cdleme28a  40352  cdlemefs44  40408  cdlemefs45ee  40412  cdleme32b  40424  cdleme32c  40425  cdleme32e  40427  cdleme35sn2aw  40440  cdleme37m  40444  cdleme39n  40448  cdleme40n  40450  cdleme40w  40452  cdleme42k  40466  cdlemeg47rv2  40492  cdlemeg46rjgN  40504  cdlemeg46rgv  40510  cdlemeg46req  40511  cdlemg2fv2  40582  cdlemg17h  40650  cdlemg31b0a  40677  cdlemg27b  40678  cdlemg31d  40682  cdlemg28b  40685  cdlemg28  40686  cdlemg29  40687  cdlemg33a  40688  cdlemg33b  40689  cdlemg33c  40690  cdlemg33d  40691  cdlemg33e  40692  cdlemg44a  40713  cdlemk7u-2N  40870  cdlemk11u-2N  40871  cdlemk12u-2N  40872  cdlemk26-3  40888  cdlemk27-3  40889  cdlemkfid3N  40907  cdlemn2  41177  cdlemn10  41188  cdlemn11c  41191