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  9745  ax5seglem6  28918  segconeu  36034  3atlem2  39508  lplncvrlvol2  39639  paddasslem15  39858  4atex  40100  trlval4  40212  cdlemc5  40219  cdlemc6  40220  cdlemd2  40223  cdlemd3  40224  cdlemd4  40225  cdleme0moN  40249  cdleme3g  40258  cdleme3h  40259  cdleme3  40261  cdleme11g  40289  cdleme11h  40290  cdleme11j  40291  cdleme11k  40292  cdleme11l  40293  cdleme11  40294  cdleme14  40297  cdleme15a  40298  cdleme15c  40300  cdleme15d  40301  cdleme15  40302  cdleme16b  40303  cdleme16c  40304  cdleme16d  40305  cdleme16e  40306  cdleme16f  40307  cdleme18a  40315  cdleme18b  40316  cdleme18c  40317  cdleme19b  40328  cdleme19e  40331  cdleme20bN  40334  cdleme20c  40335  cdleme20d  40336  cdleme20e  40337  cdleme20f  40338  cdleme20g  40339  cdleme20h  40340  cdleme20j  40342  cdleme20l2  40345  cdleme20l  40346  cdleme20m  40347  cdleme21ct  40353  cdleme22d  40367  cdleme22e  40368  cdleme22eALTN  40369  cdleme26e  40383  cdleme27a  40391  cdleme28a  40394  cdleme30a  40402  cdleme43fsv1snlem  40444  cdlemefs44  40450  cdlemefs45ee  40454  cdleme35sn2aw  40482  cdleme36a  40484  cdleme39n  40490  cdleme40m  40491  cdleme42k  40508  cdlemeg47rv2  40534  cdlemeg46frv  40549  cdlemeg46vrg  40551  cdlemeg46rgv  40552  cdlemeg46req  40553  cdlemg2fv2  40624  cdlemg4g  40640  cdlemg4  40641  cdlemg6c  40644  cdlemg8b  40652  cdlemg8c  40653  cdlemg9a  40656  cdlemg9b  40657  cdlemg9  40658  cdlemg12a  40667  cdlemg12b  40668  cdlemg12c  40669  cdlemg17h  40692  cdlemg18b  40703  cdlemg18c  40704  cdlemg31b0a  40719  cdlemg27b  40720  cdlemg31d  40724  cdlemg28b  40727  cdlemg33a  40730  cdlemg33b  40731  cdlemg33c  40732  cdlemg33d  40733  cdlemg33e  40734  cdlemg33  40735  cdlemh  40841  cdlemk6  40861  cdlemki  40865  cdlemksat  40870  cdlemksv2  40871  cdlemk7  40872  cdlemk11  40873  cdlemk12  40874  cdlemkole  40877  cdlemk14  40878  cdlemk15  40879  cdlemk17  40882  cdlemk1u  40883  cdlemk5u  40885  cdlemk6u  40886  cdlemk7u  40894  cdlemk11u  40895  cdlemk12u  40896  cdlemk7u-2N  40912  cdlemk11u-2N  40913  cdlemk12u-2N  40914  cdlemk20-2N  40916  cdlemk28-3  40932  cdlemk33N  40933  cdlemk34  40934  cdlemk37  40938  cdlemk39  40940  cdlemk35s  40961  cdlemk39s  40963  cdlemk47  40973  cdlemk48  40974  cdlemk50  40976  cdlemk51  40977  cdlemk52  40978  cdlemkyyN  40986  cdlemk43N  40987  cdlemn2  41219  cdlemn10  41230