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 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ttrclselem2  9484  ax5seglem6  27302  segconeu  34313  3atlem2  37498  lplncvrlvol2  37629  paddasslem15  37848  4atex  38090  trlval4  38202  cdlemc5  38209  cdlemc6  38210  cdlemd2  38213  cdlemd3  38214  cdlemd4  38215  cdleme0moN  38239  cdleme3g  38248  cdleme3h  38249  cdleme3  38251  cdleme11g  38279  cdleme11h  38280  cdleme11j  38281  cdleme11k  38282  cdleme11l  38283  cdleme11  38284  cdleme14  38287  cdleme15a  38288  cdleme15c  38290  cdleme15d  38291  cdleme15  38292  cdleme16b  38293  cdleme16c  38294  cdleme16d  38295  cdleme16e  38296  cdleme16f  38297  cdleme18a  38305  cdleme18b  38306  cdleme18c  38307  cdleme19b  38318  cdleme19e  38321  cdleme20bN  38324  cdleme20c  38325  cdleme20d  38326  cdleme20e  38327  cdleme20f  38328  cdleme20g  38329  cdleme20h  38330  cdleme20j  38332  cdleme20l2  38335  cdleme20l  38336  cdleme20m  38337  cdleme21ct  38343  cdleme22d  38357  cdleme22e  38358  cdleme22eALTN  38359  cdleme26e  38373  cdleme27a  38381  cdleme28a  38384  cdleme30a  38392  cdleme43fsv1snlem  38434  cdlemefs44  38440  cdlemefs45ee  38444  cdleme35sn2aw  38472  cdleme36a  38474  cdleme39n  38480  cdleme40m  38481  cdleme42k  38498  cdlemeg47rv2  38524  cdlemeg46frv  38539  cdlemeg46vrg  38541  cdlemeg46rgv  38542  cdlemeg46req  38543  cdlemg2fv2  38614  cdlemg4g  38630  cdlemg4  38631  cdlemg6c  38634  cdlemg8b  38642  cdlemg8c  38643  cdlemg9a  38646  cdlemg9b  38647  cdlemg9  38648  cdlemg12a  38657  cdlemg12b  38658  cdlemg12c  38659  cdlemg17h  38682  cdlemg18b  38693  cdlemg18c  38694  cdlemg31b0a  38709  cdlemg27b  38710  cdlemg31d  38714  cdlemg28b  38717  cdlemg33a  38720  cdlemg33b  38721  cdlemg33c  38722  cdlemg33d  38723  cdlemg33e  38724  cdlemg33  38725  cdlemh  38831  cdlemk6  38851  cdlemki  38855  cdlemksat  38860  cdlemksv2  38861  cdlemk7  38862  cdlemk11  38863  cdlemk12  38864  cdlemkole  38867  cdlemk14  38868  cdlemk15  38869  cdlemk17  38872  cdlemk1u  38873  cdlemk5u  38875  cdlemk6u  38876  cdlemk7u  38884  cdlemk11u  38885  cdlemk12u  38886  cdlemk7u-2N  38902  cdlemk11u-2N  38903  cdlemk12u-2N  38904  cdlemk20-2N  38906  cdlemk28-3  38922  cdlemk33N  38923  cdlemk34  38924  cdlemk37  38928  cdlemk39  38930  cdlemk35s  38951  cdlemk39s  38953  cdlemk47  38963  cdlemk48  38964  cdlemk50  38966  cdlemk51  38967  cdlemk52  38968  cdlemkyyN  38976  cdlemk43N  38977  cdlemn2  39209  cdlemn10  39220