Theorem simp22l 1290

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

Assertion

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

Proof of Theorem simp22l

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  ax5seglem6  27205  ttrclselem2  33712  segconeu  34240  3atlem2  37425  lplncvrlvol2  37556  paddasslem15  37775  4atex  38017  trlval4  38129  cdlemc5  38136  cdlemc6  38137  cdlemd2  38140  cdlemd3  38141  cdlemd4  38142  cdleme0moN  38166  cdleme3g  38175  cdleme3h  38176  cdleme3  38178  cdleme11g  38206  cdleme11h  38207  cdleme11j  38208  cdleme11k  38209  cdleme11l  38210  cdleme11  38211  cdleme14  38214  cdleme15a  38215  cdleme15c  38217  cdleme15d  38218  cdleme15  38219  cdleme16b  38220  cdleme16c  38221  cdleme16d  38222  cdleme16e  38223  cdleme16f  38224  cdleme18a  38232  cdleme18b  38233  cdleme18c  38234  cdleme19b  38245  cdleme19e  38248  cdleme20bN  38251  cdleme20c  38252  cdleme20d  38253  cdleme20e  38254  cdleme20f  38255  cdleme20g  38256  cdleme20h  38257  cdleme20j  38259  cdleme20l2  38262  cdleme20l  38263  cdleme20m  38264  cdleme21ct  38270  cdleme22d  38284  cdleme22e  38285  cdleme22eALTN  38286  cdleme26e  38300  cdleme27a  38308  cdleme28a  38311  cdleme30a  38319  cdleme43fsv1snlem  38361  cdlemefs44  38367  cdlemefs45ee  38371  cdleme35sn2aw  38399  cdleme36a  38401  cdleme39n  38407  cdleme40m  38408  cdleme42k  38425  cdlemeg47rv2  38451  cdlemeg46frv  38466  cdlemeg46vrg  38468  cdlemeg46rgv  38469  cdlemeg46req  38470  cdlemg2fv2  38541  cdlemg4g  38557  cdlemg4  38558  cdlemg6c  38561  cdlemg8b  38569  cdlemg8c  38570  cdlemg9a  38573  cdlemg9b  38574  cdlemg9  38575  cdlemg12a  38584  cdlemg12b  38585  cdlemg12c  38586  cdlemg17h  38609  cdlemg18b  38620  cdlemg18c  38621  cdlemg31b0a  38636  cdlemg27b  38637  cdlemg31d  38641  cdlemg28b  38644  cdlemg33a  38647  cdlemg33b  38648  cdlemg33c  38649  cdlemg33d  38650  cdlemg33e  38651  cdlemg33  38652  cdlemh  38758  cdlemk6  38778  cdlemki  38782  cdlemksat  38787  cdlemksv2  38788  cdlemk7  38789  cdlemk11  38790  cdlemk12  38791  cdlemkole  38794  cdlemk14  38795  cdlemk15  38796  cdlemk17  38799  cdlemk1u  38800  cdlemk5u  38802  cdlemk6u  38803  cdlemk7u  38811  cdlemk11u  38812  cdlemk12u  38813  cdlemk7u-2N  38829  cdlemk11u-2N  38830  cdlemk12u-2N  38831  cdlemk20-2N  38833  cdlemk28-3  38849  cdlemk33N  38850  cdlemk34  38851  cdlemk37  38855  cdlemk39  38857  cdlemk35s  38878  cdlemk39s  38880  cdlemk47  38890  cdlemk48  38891  cdlemk50  38893  cdlemk51  38894  cdlemk52  38895  cdlemkyyN  38903  cdlemk43N  38904  cdlemn2  39136  cdlemn10  39147