Theorem simp22l 1311

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

Assertion

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

Proof of Theorem simp22l

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ttrclselem2  9757  ax5seglem6  29545  segconeu  36967  3atlem2  40744  lplncvrlvol2  40875  paddasslem15  41094  4atex  41336  trlval4  41448  cdlemc5  41455  cdlemc6  41456  cdlemd2  41459  cdlemd3  41460  cdlemd4  41461  cdleme0moN  41485  cdleme3g  41494  cdleme3h  41495  cdleme3  41497  cdleme11g  41525  cdleme11h  41526  cdleme11j  41527  cdleme11k  41528  cdleme11l  41529  cdleme11  41530  cdleme14  41533  cdleme15a  41534  cdleme15c  41536  cdleme15d  41537  cdleme15  41538  cdleme16b  41539  cdleme16c  41540  cdleme16d  41541  cdleme16e  41542  cdleme16f  41543  cdleme18a  41551  cdleme18b  41552  cdleme18c  41553  cdleme19b  41564  cdleme19e  41567  cdleme20bN  41570  cdleme20c  41571  cdleme20d  41572  cdleme20e  41573  cdleme20f  41574  cdleme20g  41575  cdleme20h  41576  cdleme20j  41578  cdleme20l2  41581  cdleme20l  41582  cdleme20m  41583  cdleme21ct  41589  cdleme22d  41603  cdleme22e  41604  cdleme22eALTN  41605  cdleme26e  41619  cdleme27a  41627  cdleme28a  41630  cdleme30a  41638  cdleme43fsv1snlem  41680  cdlemefs44  41686  cdlemefs45ee  41690  cdleme35sn2aw  41718  cdleme36a  41720  cdleme39n  41726  cdleme40m  41727  cdleme42k  41744  cdlemeg47rv2  41770  cdlemeg46frv  41785  cdlemeg46vrg  41787  cdlemeg46rgv  41788  cdlemeg46req  41789  cdlemg2fv2  41860  cdlemg4g  41876  cdlemg4  41877  cdlemg6c  41880  cdlemg8b  41888  cdlemg8c  41889  cdlemg9a  41892  cdlemg9b  41893  cdlemg9  41894  cdlemg12a  41903  cdlemg12b  41904  cdlemg12c  41905  cdlemg17h  41928  cdlemg18b  41939  cdlemg18c  41940  cdlemg31b0a  41955  cdlemg27b  41956  cdlemg31d  41960  cdlemg28b  41963  cdlemg33a  41966  cdlemg33b  41967  cdlemg33c  41968  cdlemg33d  41969  cdlemg33e  41970  cdlemg33  41971  cdlemh  42077  cdlemk6  42097  cdlemki  42101  cdlemksat  42106  cdlemksv2  42107  cdlemk7  42108  cdlemk11  42109  cdlemk12  42110  cdlemkole  42113  cdlemk14  42114  cdlemk15  42115  cdlemk17  42118  cdlemk1u  42119  cdlemk5u  42121  cdlemk6u  42122  cdlemk7u  42130  cdlemk11u  42131  cdlemk12u  42132  cdlemk7u-2N  42148  cdlemk11u-2N  42149  cdlemk12u-2N  42150  cdlemk20-2N  42152  cdlemk28-3  42168  cdlemk33N  42169  cdlemk34  42170  cdlemk37  42174  cdlemk39  42176  cdlemk35s  42197  cdlemk39s  42199  cdlemk47  42209  cdlemk48  42210  cdlemk50  42212  cdlemk51  42213  cdlemk52  42214  cdlemkyyN  42222  cdlemk43N  42223  cdlemn2  42455  cdlemn10  42466