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 1135	1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜑)

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

This theorem is referenced by:  ttrclselem2  9647  ax5seglem6  29019  segconeu  36224  3atlem2  39854  lplncvrlvol2  39985  paddasslem15  40204  4atex  40446  trlval4  40558  cdlemc5  40565  cdlemc6  40566  cdlemd2  40569  cdlemd3  40570  cdlemd4  40571  cdleme0moN  40595  cdleme3g  40604  cdleme3h  40605  cdleme3  40607  cdleme11g  40635  cdleme11h  40636  cdleme11j  40637  cdleme11k  40638  cdleme11l  40639  cdleme11  40640  cdleme14  40643  cdleme15a  40644  cdleme15c  40646  cdleme15d  40647  cdleme15  40648  cdleme16b  40649  cdleme16c  40650  cdleme16d  40651  cdleme16e  40652  cdleme16f  40653  cdleme18a  40661  cdleme18b  40662  cdleme18c  40663  cdleme19b  40674  cdleme19e  40677  cdleme20bN  40680  cdleme20c  40681  cdleme20d  40682  cdleme20e  40683  cdleme20f  40684  cdleme20g  40685  cdleme20h  40686  cdleme20j  40688  cdleme20l2  40691  cdleme20l  40692  cdleme20m  40693  cdleme21ct  40699  cdleme22d  40713  cdleme22e  40714  cdleme22eALTN  40715  cdleme26e  40729  cdleme27a  40737  cdleme28a  40740  cdleme30a  40748  cdleme43fsv1snlem  40790  cdlemefs44  40796  cdlemefs45ee  40800  cdleme35sn2aw  40828  cdleme36a  40830  cdleme39n  40836  cdleme40m  40837  cdleme42k  40854  cdlemeg47rv2  40880  cdlemeg46frv  40895  cdlemeg46vrg  40897  cdlemeg46rgv  40898  cdlemeg46req  40899  cdlemg2fv2  40970  cdlemg4g  40986  cdlemg4  40987  cdlemg6c  40990  cdlemg8b  40998  cdlemg8c  40999  cdlemg9a  41002  cdlemg9b  41003  cdlemg9  41004  cdlemg12a  41013  cdlemg12b  41014  cdlemg12c  41015  cdlemg17h  41038  cdlemg18b  41049  cdlemg18c  41050  cdlemg31b0a  41065  cdlemg27b  41066  cdlemg31d  41070  cdlemg28b  41073  cdlemg33a  41076  cdlemg33b  41077  cdlemg33c  41078  cdlemg33d  41079  cdlemg33e  41080  cdlemg33  41081  cdlemh  41187  cdlemk6  41207  cdlemki  41211  cdlemksat  41216  cdlemksv2  41217  cdlemk7  41218  cdlemk11  41219  cdlemk12  41220  cdlemkole  41223  cdlemk14  41224  cdlemk15  41225  cdlemk17  41228  cdlemk1u  41229  cdlemk5u  41231  cdlemk6u  41232  cdlemk7u  41240  cdlemk11u  41241  cdlemk12u  41242  cdlemk7u-2N  41258  cdlemk11u-2N  41259  cdlemk12u-2N  41260  cdlemk20-2N  41262  cdlemk28-3  41278  cdlemk33N  41279  cdlemk34  41280  cdlemk37  41284  cdlemk39  41286  cdlemk35s  41307  cdlemk39s  41309  cdlemk47  41319  cdlemk48  41320  cdlemk50  41322  cdlemk51  41323  cdlemk52  41324  cdlemkyyN  41332  cdlemk43N  41333  cdlemn2  41565  cdlemn10  41576