Theorem simp22l 1288

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

Assertion

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

Proof of Theorem simp22l

Step	Hyp	Ref	Expression
1		simp2l 1195	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜑)
2	1	3ad2ant2 1130	1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  ax5seglem6  26714  segconeu  33467  3atlem2  36614  lplncvrlvol2  36745  paddasslem15  36964  4atex  37206  trlval4  37318  cdlemc5  37325  cdlemc6  37326  cdlemd2  37329  cdlemd3  37330  cdlemd4  37331  cdleme0moN  37355  cdleme3g  37364  cdleme3h  37365  cdleme3  37367  cdleme11g  37395  cdleme11h  37396  cdleme11j  37397  cdleme11k  37398  cdleme11l  37399  cdleme11  37400  cdleme14  37403  cdleme15a  37404  cdleme15c  37406  cdleme15d  37407  cdleme15  37408  cdleme16b  37409  cdleme16c  37410  cdleme16d  37411  cdleme16e  37412  cdleme16f  37413  cdleme18a  37421  cdleme18b  37422  cdleme18c  37423  cdleme19b  37434  cdleme19e  37437  cdleme20bN  37440  cdleme20c  37441  cdleme20d  37442  cdleme20e  37443  cdleme20f  37444  cdleme20g  37445  cdleme20h  37446  cdleme20j  37448  cdleme20l2  37451  cdleme20l  37452  cdleme20m  37453  cdleme21ct  37459  cdleme22d  37473  cdleme22e  37474  cdleme22eALTN  37475  cdleme26e  37489  cdleme27a  37497  cdleme28a  37500  cdleme30a  37508  cdleme43fsv1snlem  37550  cdlemefs44  37556  cdlemefs45ee  37560  cdleme35sn2aw  37588  cdleme36a  37590  cdleme39n  37596  cdleme40m  37597  cdleme42k  37614  cdlemeg47rv2  37640  cdlemeg46frv  37655  cdlemeg46vrg  37657  cdlemeg46rgv  37658  cdlemeg46req  37659  cdlemg2fv2  37730  cdlemg4g  37746  cdlemg4  37747  cdlemg6c  37750  cdlemg8b  37758  cdlemg8c  37759  cdlemg9a  37762  cdlemg9b  37763  cdlemg9  37764  cdlemg12a  37773  cdlemg12b  37774  cdlemg12c  37775  cdlemg17h  37798  cdlemg18b  37809  cdlemg18c  37810  cdlemg31b0a  37825  cdlemg27b  37826  cdlemg31d  37830  cdlemg28b  37833  cdlemg33a  37836  cdlemg33b  37837  cdlemg33c  37838  cdlemg33d  37839  cdlemg33e  37840  cdlemg33  37841  cdlemh  37947  cdlemk6  37967  cdlemki  37971  cdlemksat  37976  cdlemksv2  37977  cdlemk7  37978  cdlemk11  37979  cdlemk12  37980  cdlemkole  37983  cdlemk14  37984  cdlemk15  37985  cdlemk17  37988  cdlemk1u  37989  cdlemk5u  37991  cdlemk6u  37992  cdlemk7u  38000  cdlemk11u  38001  cdlemk12u  38002  cdlemk7u-2N  38018  cdlemk11u-2N  38019  cdlemk12u-2N  38020  cdlemk20-2N  38022  cdlemk28-3  38038  cdlemk33N  38039  cdlemk34  38040  cdlemk37  38044  cdlemk39  38046  cdlemk35s  38067  cdlemk39s  38069  cdlemk47  38079  cdlemk48  38080  cdlemk50  38082  cdlemk51  38083  cdlemk52  38084  cdlemkyyN  38092  cdlemk43N  38093  cdlemn2  38325  cdlemn10  38336