Theorem simp22l 1299

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

Assertion

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

Proof of Theorem simp22l

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  ttrclselem2  9645  ax5seglem6  29028  segconeu  36246  3atlem2  39983  lplncvrlvol2  40114  paddasslem15  40333  4atex  40575  trlval4  40687  cdlemc5  40694  cdlemc6  40695  cdlemd2  40698  cdlemd3  40699  cdlemd4  40700  cdleme0moN  40724  cdleme3g  40733  cdleme3h  40734  cdleme3  40736  cdleme11g  40764  cdleme11h  40765  cdleme11j  40766  cdleme11k  40767  cdleme11l  40768  cdleme11  40769  cdleme14  40772  cdleme15a  40773  cdleme15c  40775  cdleme15d  40776  cdleme15  40777  cdleme16b  40778  cdleme16c  40779  cdleme16d  40780  cdleme16e  40781  cdleme16f  40782  cdleme18a  40790  cdleme18b  40791  cdleme18c  40792  cdleme19b  40803  cdleme19e  40806  cdleme20bN  40809  cdleme20c  40810  cdleme20d  40811  cdleme20e  40812  cdleme20f  40813  cdleme20g  40814  cdleme20h  40815  cdleme20j  40817  cdleme20l2  40820  cdleme20l  40821  cdleme20m  40822  cdleme21ct  40828  cdleme22d  40842  cdleme22e  40843  cdleme22eALTN  40844  cdleme26e  40858  cdleme27a  40866  cdleme28a  40869  cdleme30a  40877  cdleme43fsv1snlem  40919  cdlemefs44  40925  cdlemefs45ee  40929  cdleme35sn2aw  40957  cdleme36a  40959  cdleme39n  40965  cdleme40m  40966  cdleme42k  40983  cdlemeg47rv2  41009  cdlemeg46frv  41024  cdlemeg46vrg  41026  cdlemeg46rgv  41027  cdlemeg46req  41028  cdlemg2fv2  41099  cdlemg4g  41115  cdlemg4  41116  cdlemg6c  41119  cdlemg8b  41127  cdlemg8c  41128  cdlemg9a  41131  cdlemg9b  41132  cdlemg9  41133  cdlemg12a  41142  cdlemg12b  41143  cdlemg12c  41144  cdlemg17h  41167  cdlemg18b  41178  cdlemg18c  41179  cdlemg31b0a  41194  cdlemg27b  41195  cdlemg31d  41199  cdlemg28b  41202  cdlemg33a  41205  cdlemg33b  41206  cdlemg33c  41207  cdlemg33d  41208  cdlemg33e  41209  cdlemg33  41210  cdlemh  41316  cdlemk6  41336  cdlemki  41340  cdlemksat  41345  cdlemksv2  41346  cdlemk7  41347  cdlemk11  41348  cdlemk12  41349  cdlemkole  41352  cdlemk14  41353  cdlemk15  41354  cdlemk17  41357  cdlemk1u  41358  cdlemk5u  41360  cdlemk6u  41361  cdlemk7u  41369  cdlemk11u  41370  cdlemk12u  41371  cdlemk7u-2N  41387  cdlemk11u-2N  41388  cdlemk12u-2N  41389  cdlemk20-2N  41391  cdlemk28-3  41407  cdlemk33N  41408  cdlemk34  41409  cdlemk37  41413  cdlemk39  41415  cdlemk35s  41436  cdlemk39s  41438  cdlemk47  41448  cdlemk48  41449  cdlemk50  41451  cdlemk51  41452  cdlemk52  41453  cdlemkyyN  41461  cdlemk43N  41462  cdlemn2  41694  cdlemn10  41705