Theorem simp23l 1294

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

Assertion

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

Proof of Theorem simp23l

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  ax5seglem6  28447  lshpkrlem5  38287  lplnexllnN  38738  4atexlemt  39227  4atex2  39251  4atex3  39255  trlval4  39362  cdlemc5  39369  cdlemc6  39370  cdlemd2  39373  cdleme0e  39391  cdleme0moN  39399  cdleme3g  39408  cdleme3h  39409  cdleme3  39411  cdleme4  39412  cdleme5  39414  cdleme9  39427  cdleme11fN  39438  cdleme11j  39441  cdleme11k  39442  cdleme11l  39443  cdleme11  39444  cdleme14  39447  cdleme15a  39448  cdleme15b  39449  cdleme15c  39450  cdleme16b  39453  cdleme16c  39454  cdleme16d  39455  cdleme16e  39456  cdleme16f  39457  cdleme17d1  39463  cdleme18c  39467  cdlemednpq  39473  cdleme19c  39479  cdleme20bN  39484  cdleme20d  39486  cdleme20f  39488  cdleme20g  39489  cdleme20h  39490  cdleme20j  39492  cdleme20l2  39495  cdleme20l  39496  cdleme20m  39497  cdleme22cN  39516  cdleme22d  39517  cdleme22e  39518  cdleme22f  39520  cdleme26fALTN  39536  cdleme26f  39537  cdleme26f2ALTN  39538  cdleme26f2  39539  cdleme27a  39541  cdleme28a  39544  cdlemefs44  39600  cdlemefs45ee  39604  cdleme32b  39616  cdleme32c  39617  cdleme32e  39619  cdleme35sn2aw  39632  cdleme37m  39636  cdleme39n  39640  cdleme40n  39642  cdleme40w  39644  cdleme42k  39658  cdlemeg47rv2  39684  cdlemeg46rjgN  39696  cdlemeg46rgv  39702  cdlemeg46req  39703  cdlemg2fv2  39774  cdlemg17h  39842  cdlemg31b0a  39869  cdlemg27b  39870  cdlemg31d  39874  cdlemg28b  39877  cdlemg28  39878  cdlemg29  39879  cdlemg33a  39880  cdlemg33b  39881  cdlemg33c  39882  cdlemg33d  39883  cdlemg33e  39884  cdlemg44a  39905  cdlemk7u-2N  40062  cdlemk11u-2N  40063  cdlemk12u-2N  40064  cdlemk26-3  40080  cdlemk27-3  40081  cdlemkfid3N  40099  cdlemn2  40369  cdlemn10  40380  cdlemn11c  40383