Theorem simp23l 1295

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

Assertion

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

Proof of Theorem simp23l

Step	Hyp	Ref	Expression
1		simp3l 1202	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant2 1134	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  28914  lshpkrlem5  39233  lplnexllnN  39683  4atexlemt  40172  4atex2  40196  4atex3  40200  trlval4  40307  cdlemc5  40314  cdlemc6  40315  cdlemd2  40318  cdleme0e  40336  cdleme0moN  40344  cdleme3g  40353  cdleme3h  40354  cdleme3  40356  cdleme4  40357  cdleme5  40359  cdleme9  40372  cdleme11fN  40383  cdleme11j  40386  cdleme11k  40387  cdleme11l  40388  cdleme11  40389  cdleme14  40392  cdleme15a  40393  cdleme15b  40394  cdleme15c  40395  cdleme16b  40398  cdleme16c  40399  cdleme16d  40400  cdleme16e  40401  cdleme16f  40402  cdleme17d1  40408  cdleme18c  40412  cdlemednpq  40418  cdleme19c  40424  cdleme20bN  40429  cdleme20d  40431  cdleme20f  40433  cdleme20g  40434  cdleme20h  40435  cdleme20j  40437  cdleme20l2  40440  cdleme20l  40441  cdleme20m  40442  cdleme22cN  40461  cdleme22d  40462  cdleme22e  40463  cdleme22f  40465  cdleme26fALTN  40481  cdleme26f  40482  cdleme26f2ALTN  40483  cdleme26f2  40484  cdleme27a  40486  cdleme28a  40489  cdlemefs44  40545  cdlemefs45ee  40549  cdleme32b  40561  cdleme32c  40562  cdleme32e  40564  cdleme35sn2aw  40577  cdleme37m  40581  cdleme39n  40585  cdleme40n  40587  cdleme40w  40589  cdleme42k  40603  cdlemeg47rv2  40629  cdlemeg46rjgN  40641  cdlemeg46rgv  40647  cdlemeg46req  40648  cdlemg2fv2  40719  cdlemg17h  40787  cdlemg31b0a  40814  cdlemg27b  40815  cdlemg31d  40819  cdlemg28b  40822  cdlemg28  40823  cdlemg29  40824  cdlemg33a  40825  cdlemg33b  40826  cdlemg33c  40827  cdlemg33d  40828  cdlemg33e  40829  cdlemg44a  40850  cdlemk7u-2N  41007  cdlemk11u-2N  41008  cdlemk12u-2N  41009  cdlemk26-3  41025  cdlemk27-3  41026  cdlemkfid3N  41044  cdlemn2  41314  cdlemn10  41325  cdlemn11c  41328