Theorem simp22l 1294

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

Assertion

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

Proof of Theorem simp22l

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  ax5seglem6  27025  segconeu  34050  3atlem2  37235  lplncvrlvol2  37366  paddasslem15  37585  4atex  37827  trlval4  37939  cdlemc5  37946  cdlemc6  37947  cdlemd2  37950  cdlemd3  37951  cdlemd4  37952  cdleme0moN  37976  cdleme3g  37985  cdleme3h  37986  cdleme3  37988  cdleme11g  38016  cdleme11h  38017  cdleme11j  38018  cdleme11k  38019  cdleme11l  38020  cdleme11  38021  cdleme14  38024  cdleme15a  38025  cdleme15c  38027  cdleme15d  38028  cdleme15  38029  cdleme16b  38030  cdleme16c  38031  cdleme16d  38032  cdleme16e  38033  cdleme16f  38034  cdleme18a  38042  cdleme18b  38043  cdleme18c  38044  cdleme19b  38055  cdleme19e  38058  cdleme20bN  38061  cdleme20c  38062  cdleme20d  38063  cdleme20e  38064  cdleme20f  38065  cdleme20g  38066  cdleme20h  38067  cdleme20j  38069  cdleme20l2  38072  cdleme20l  38073  cdleme20m  38074  cdleme21ct  38080  cdleme22d  38094  cdleme22e  38095  cdleme22eALTN  38096  cdleme26e  38110  cdleme27a  38118  cdleme28a  38121  cdleme30a  38129  cdleme43fsv1snlem  38171  cdlemefs44  38177  cdlemefs45ee  38181  cdleme35sn2aw  38209  cdleme36a  38211  cdleme39n  38217  cdleme40m  38218  cdleme42k  38235  cdlemeg47rv2  38261  cdlemeg46frv  38276  cdlemeg46vrg  38278  cdlemeg46rgv  38279  cdlemeg46req  38280  cdlemg2fv2  38351  cdlemg4g  38367  cdlemg4  38368  cdlemg6c  38371  cdlemg8b  38379  cdlemg8c  38380  cdlemg9a  38383  cdlemg9b  38384  cdlemg9  38385  cdlemg12a  38394  cdlemg12b  38395  cdlemg12c  38396  cdlemg17h  38419  cdlemg18b  38430  cdlemg18c  38431  cdlemg31b0a  38446  cdlemg27b  38447  cdlemg31d  38451  cdlemg28b  38454  cdlemg33a  38457  cdlemg33b  38458  cdlemg33c  38459  cdlemg33d  38460  cdlemg33e  38461  cdlemg33  38462  cdlemh  38568  cdlemk6  38588  cdlemki  38592  cdlemksat  38597  cdlemksv2  38598  cdlemk7  38599  cdlemk11  38600  cdlemk12  38601  cdlemkole  38604  cdlemk14  38605  cdlemk15  38606  cdlemk17  38609  cdlemk1u  38610  cdlemk5u  38612  cdlemk6u  38613  cdlemk7u  38621  cdlemk11u  38622  cdlemk12u  38623  cdlemk7u-2N  38639  cdlemk11u-2N  38640  cdlemk12u-2N  38641  cdlemk20-2N  38643  cdlemk28-3  38659  cdlemk33N  38660  cdlemk34  38661  cdlemk37  38665  cdlemk39  38667  cdlemk35s  38688  cdlemk39s  38690  cdlemk47  38700  cdlemk48  38701  cdlemk50  38703  cdlemk51  38704  cdlemk52  38705  cdlemkyyN  38713  cdlemk43N  38714  cdlemn2  38946  cdlemn10  38957