Theorem simp22l 1291

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

Assertion

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

Proof of Theorem simp22l

Step	Hyp	Ref	Expression
1		simp2l 1198	. 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:  ttrclselem2  9764  ax5seglem6  28964  segconeu  35993  3atlem2  39467  lplncvrlvol2  39598  paddasslem15  39817  4atex  40059  trlval4  40171  cdlemc5  40178  cdlemc6  40179  cdlemd2  40182  cdlemd3  40183  cdlemd4  40184  cdleme0moN  40208  cdleme3g  40217  cdleme3h  40218  cdleme3  40220  cdleme11g  40248  cdleme11h  40249  cdleme11j  40250  cdleme11k  40251  cdleme11l  40252  cdleme11  40253  cdleme14  40256  cdleme15a  40257  cdleme15c  40259  cdleme15d  40260  cdleme15  40261  cdleme16b  40262  cdleme16c  40263  cdleme16d  40264  cdleme16e  40265  cdleme16f  40266  cdleme18a  40274  cdleme18b  40275  cdleme18c  40276  cdleme19b  40287  cdleme19e  40290  cdleme20bN  40293  cdleme20c  40294  cdleme20d  40295  cdleme20e  40296  cdleme20f  40297  cdleme20g  40298  cdleme20h  40299  cdleme20j  40301  cdleme20l2  40304  cdleme20l  40305  cdleme20m  40306  cdleme21ct  40312  cdleme22d  40326  cdleme22e  40327  cdleme22eALTN  40328  cdleme26e  40342  cdleme27a  40350  cdleme28a  40353  cdleme30a  40361  cdleme43fsv1snlem  40403  cdlemefs44  40409  cdlemefs45ee  40413  cdleme35sn2aw  40441  cdleme36a  40443  cdleme39n  40449  cdleme40m  40450  cdleme42k  40467  cdlemeg47rv2  40493  cdlemeg46frv  40508  cdlemeg46vrg  40510  cdlemeg46rgv  40511  cdlemeg46req  40512  cdlemg2fv2  40583  cdlemg4g  40599  cdlemg4  40600  cdlemg6c  40603  cdlemg8b  40611  cdlemg8c  40612  cdlemg9a  40615  cdlemg9b  40616  cdlemg9  40617  cdlemg12a  40626  cdlemg12b  40627  cdlemg12c  40628  cdlemg17h  40651  cdlemg18b  40662  cdlemg18c  40663  cdlemg31b0a  40678  cdlemg27b  40679  cdlemg31d  40683  cdlemg28b  40686  cdlemg33a  40689  cdlemg33b  40690  cdlemg33c  40691  cdlemg33d  40692  cdlemg33e  40693  cdlemg33  40694  cdlemh  40800  cdlemk6  40820  cdlemki  40824  cdlemksat  40829  cdlemksv2  40830  cdlemk7  40831  cdlemk11  40832  cdlemk12  40833  cdlemkole  40836  cdlemk14  40837  cdlemk15  40838  cdlemk17  40841  cdlemk1u  40842  cdlemk5u  40844  cdlemk6u  40845  cdlemk7u  40853  cdlemk11u  40854  cdlemk12u  40855  cdlemk7u-2N  40871  cdlemk11u-2N  40872  cdlemk12u-2N  40873  cdlemk20-2N  40875  cdlemk28-3  40891  cdlemk33N  40892  cdlemk34  40893  cdlemk37  40897  cdlemk39  40899  cdlemk35s  40920  cdlemk39s  40922  cdlemk47  40932  cdlemk48  40933  cdlemk50  40935  cdlemk51  40936  cdlemk52  40937  cdlemkyyN  40945  cdlemk43N  40946  cdlemn2  41178  cdlemn10  41189