Theorem simp22l 1293

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

Assertion

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

Proof of Theorem simp22l

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

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

This theorem is referenced by:  ttrclselem2  9679  ax5seglem6  28861  segconeu  35999  3atlem2  39478  lplncvrlvol2  39609  paddasslem15  39828  4atex  40070  trlval4  40182  cdlemc5  40189  cdlemc6  40190  cdlemd2  40193  cdlemd3  40194  cdlemd4  40195  cdleme0moN  40219  cdleme3g  40228  cdleme3h  40229  cdleme3  40231  cdleme11g  40259  cdleme11h  40260  cdleme11j  40261  cdleme11k  40262  cdleme11l  40263  cdleme11  40264  cdleme14  40267  cdleme15a  40268  cdleme15c  40270  cdleme15d  40271  cdleme15  40272  cdleme16b  40273  cdleme16c  40274  cdleme16d  40275  cdleme16e  40276  cdleme16f  40277  cdleme18a  40285  cdleme18b  40286  cdleme18c  40287  cdleme19b  40298  cdleme19e  40301  cdleme20bN  40304  cdleme20c  40305  cdleme20d  40306  cdleme20e  40307  cdleme20f  40308  cdleme20g  40309  cdleme20h  40310  cdleme20j  40312  cdleme20l2  40315  cdleme20l  40316  cdleme20m  40317  cdleme21ct  40323  cdleme22d  40337  cdleme22e  40338  cdleme22eALTN  40339  cdleme26e  40353  cdleme27a  40361  cdleme28a  40364  cdleme30a  40372  cdleme43fsv1snlem  40414  cdlemefs44  40420  cdlemefs45ee  40424  cdleme35sn2aw  40452  cdleme36a  40454  cdleme39n  40460  cdleme40m  40461  cdleme42k  40478  cdlemeg47rv2  40504  cdlemeg46frv  40519  cdlemeg46vrg  40521  cdlemeg46rgv  40522  cdlemeg46req  40523  cdlemg2fv2  40594  cdlemg4g  40610  cdlemg4  40611  cdlemg6c  40614  cdlemg8b  40622  cdlemg8c  40623  cdlemg9a  40626  cdlemg9b  40627  cdlemg9  40628  cdlemg12a  40637  cdlemg12b  40638  cdlemg12c  40639  cdlemg17h  40662  cdlemg18b  40673  cdlemg18c  40674  cdlemg31b0a  40689  cdlemg27b  40690  cdlemg31d  40694  cdlemg28b  40697  cdlemg33a  40700  cdlemg33b  40701  cdlemg33c  40702  cdlemg33d  40703  cdlemg33e  40704  cdlemg33  40705  cdlemh  40811  cdlemk6  40831  cdlemki  40835  cdlemksat  40840  cdlemksv2  40841  cdlemk7  40842  cdlemk11  40843  cdlemk12  40844  cdlemkole  40847  cdlemk14  40848  cdlemk15  40849  cdlemk17  40852  cdlemk1u  40853  cdlemk5u  40855  cdlemk6u  40856  cdlemk7u  40864  cdlemk11u  40865  cdlemk12u  40866  cdlemk7u-2N  40882  cdlemk11u-2N  40883  cdlemk12u-2N  40884  cdlemk20-2N  40886  cdlemk28-3  40902  cdlemk33N  40903  cdlemk34  40904  cdlemk37  40908  cdlemk39  40910  cdlemk35s  40931  cdlemk39s  40933  cdlemk47  40943  cdlemk48  40944  cdlemk50  40946  cdlemk51  40947  cdlemk52  40948  cdlemkyyN  40956  cdlemk43N  40957  cdlemn2  41189  cdlemn10  41200