Theorem simp22l 1294

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

Assertion

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

Proof of Theorem simp22l

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

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

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 1089

This theorem is referenced by:  ttrclselem2  9638  ax5seglem6  29017  segconeu  36209  3atlem2  39944  lplncvrlvol2  40075  paddasslem15  40294  4atex  40536  trlval4  40648  cdlemc5  40655  cdlemc6  40656  cdlemd2  40659  cdlemd3  40660  cdlemd4  40661  cdleme0moN  40685  cdleme3g  40694  cdleme3h  40695  cdleme3  40697  cdleme11g  40725  cdleme11h  40726  cdleme11j  40727  cdleme11k  40728  cdleme11l  40729  cdleme11  40730  cdleme14  40733  cdleme15a  40734  cdleme15c  40736  cdleme15d  40737  cdleme15  40738  cdleme16b  40739  cdleme16c  40740  cdleme16d  40741  cdleme16e  40742  cdleme16f  40743  cdleme18a  40751  cdleme18b  40752  cdleme18c  40753  cdleme19b  40764  cdleme19e  40767  cdleme20bN  40770  cdleme20c  40771  cdleme20d  40772  cdleme20e  40773  cdleme20f  40774  cdleme20g  40775  cdleme20h  40776  cdleme20j  40778  cdleme20l2  40781  cdleme20l  40782  cdleme20m  40783  cdleme21ct  40789  cdleme22d  40803  cdleme22e  40804  cdleme22eALTN  40805  cdleme26e  40819  cdleme27a  40827  cdleme28a  40830  cdleme30a  40838  cdleme43fsv1snlem  40880  cdlemefs44  40886  cdlemefs45ee  40890  cdleme35sn2aw  40918  cdleme36a  40920  cdleme39n  40926  cdleme40m  40927  cdleme42k  40944  cdlemeg47rv2  40970  cdlemeg46frv  40985  cdlemeg46vrg  40987  cdlemeg46rgv  40988  cdlemeg46req  40989  cdlemg2fv2  41060  cdlemg4g  41076  cdlemg4  41077  cdlemg6c  41080  cdlemg8b  41088  cdlemg8c  41089  cdlemg9a  41092  cdlemg9b  41093  cdlemg9  41094  cdlemg12a  41103  cdlemg12b  41104  cdlemg12c  41105  cdlemg17h  41128  cdlemg18b  41139  cdlemg18c  41140  cdlemg31b0a  41155  cdlemg27b  41156  cdlemg31d  41160  cdlemg28b  41163  cdlemg33a  41166  cdlemg33b  41167  cdlemg33c  41168  cdlemg33d  41169  cdlemg33e  41170  cdlemg33  41171  cdlemh  41277  cdlemk6  41297  cdlemki  41301  cdlemksat  41306  cdlemksv2  41307  cdlemk7  41308  cdlemk11  41309  cdlemk12  41310  cdlemkole  41313  cdlemk14  41314  cdlemk15  41315  cdlemk17  41318  cdlemk1u  41319  cdlemk5u  41321  cdlemk6u  41322  cdlemk7u  41330  cdlemk11u  41331  cdlemk12u  41332  cdlemk7u-2N  41348  cdlemk11u-2N  41349  cdlemk12u-2N  41350  cdlemk20-2N  41352  cdlemk28-3  41368  cdlemk33N  41369  cdlemk34  41370  cdlemk37  41374  cdlemk39  41376  cdlemk35s  41397  cdlemk39s  41399  cdlemk47  41409  cdlemk48  41410  cdlemk50  41412  cdlemk51  41413  cdlemk52  41414  cdlemkyyN  41422  cdlemk43N  41423  cdlemn2  41655  cdlemn10  41666