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  9575  ax5seglem6  27504  segconeu  34404  3atlem2  37745  lplncvrlvol2  37876  paddasslem15  38095  4atex  38337  trlval4  38449  cdlemc5  38456  cdlemc6  38457  cdlemd2  38460  cdlemd3  38461  cdlemd4  38462  cdleme0moN  38486  cdleme3g  38495  cdleme3h  38496  cdleme3  38498  cdleme11g  38526  cdleme11h  38527  cdleme11j  38528  cdleme11k  38529  cdleme11l  38530  cdleme11  38531  cdleme14  38534  cdleme15a  38535  cdleme15c  38537  cdleme15d  38538  cdleme15  38539  cdleme16b  38540  cdleme16c  38541  cdleme16d  38542  cdleme16e  38543  cdleme16f  38544  cdleme18a  38552  cdleme18b  38553  cdleme18c  38554  cdleme19b  38565  cdleme19e  38568  cdleme20bN  38571  cdleme20c  38572  cdleme20d  38573  cdleme20e  38574  cdleme20f  38575  cdleme20g  38576  cdleme20h  38577  cdleme20j  38579  cdleme20l2  38582  cdleme20l  38583  cdleme20m  38584  cdleme21ct  38590  cdleme22d  38604  cdleme22e  38605  cdleme22eALTN  38606  cdleme26e  38620  cdleme27a  38628  cdleme28a  38631  cdleme30a  38639  cdleme43fsv1snlem  38681  cdlemefs44  38687  cdlemefs45ee  38691  cdleme35sn2aw  38719  cdleme36a  38721  cdleme39n  38727  cdleme40m  38728  cdleme42k  38745  cdlemeg47rv2  38771  cdlemeg46frv  38786  cdlemeg46vrg  38788  cdlemeg46rgv  38789  cdlemeg46req  38790  cdlemg2fv2  38861  cdlemg4g  38877  cdlemg4  38878  cdlemg6c  38881  cdlemg8b  38889  cdlemg8c  38890  cdlemg9a  38893  cdlemg9b  38894  cdlemg9  38895  cdlemg12a  38904  cdlemg12b  38905  cdlemg12c  38906  cdlemg17h  38929  cdlemg18b  38940  cdlemg18c  38941  cdlemg31b0a  38956  cdlemg27b  38957  cdlemg31d  38961  cdlemg28b  38964  cdlemg33a  38967  cdlemg33b  38968  cdlemg33c  38969  cdlemg33d  38970  cdlemg33e  38971  cdlemg33  38972  cdlemh  39078  cdlemk6  39098  cdlemki  39102  cdlemksat  39107  cdlemksv2  39108  cdlemk7  39109  cdlemk11  39110  cdlemk12  39111  cdlemkole  39114  cdlemk14  39115  cdlemk15  39116  cdlemk17  39119  cdlemk1u  39120  cdlemk5u  39122  cdlemk6u  39123  cdlemk7u  39131  cdlemk11u  39132  cdlemk12u  39133  cdlemk7u-2N  39149  cdlemk11u-2N  39150  cdlemk12u-2N  39151  cdlemk20-2N  39153  cdlemk28-3  39169  cdlemk33N  39170  cdlemk34  39171  cdlemk37  39175  cdlemk39  39177  cdlemk35s  39198  cdlemk39s  39200  cdlemk47  39210  cdlemk48  39211  cdlemk50  39213  cdlemk51  39214  cdlemk52  39215  cdlemkyyN  39223  cdlemk43N  39224  cdlemn2  39456  cdlemn10  39467