Theorem simp22l 1311

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

Assertion

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

Proof of Theorem simp22l

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ttrclselem2  9711  ax5seglem6  29494  segconeu  36746  3atlem2  40509  lplncvrlvol2  40640  paddasslem15  40859  4atex  41101  trlval4  41213  cdlemc5  41220  cdlemc6  41221  cdlemd2  41224  cdlemd3  41225  cdlemd4  41226  cdleme0moN  41250  cdleme3g  41259  cdleme3h  41260  cdleme3  41262  cdleme11g  41290  cdleme11h  41291  cdleme11j  41292  cdleme11k  41293  cdleme11l  41294  cdleme11  41295  cdleme14  41298  cdleme15a  41299  cdleme15c  41301  cdleme15d  41302  cdleme15  41303  cdleme16b  41304  cdleme16c  41305  cdleme16d  41306  cdleme16e  41307  cdleme16f  41308  cdleme18a  41316  cdleme18b  41317  cdleme18c  41318  cdleme19b  41329  cdleme19e  41332  cdleme20bN  41335  cdleme20c  41336  cdleme20d  41337  cdleme20e  41338  cdleme20f  41339  cdleme20g  41340  cdleme20h  41341  cdleme20j  41343  cdleme20l2  41346  cdleme20l  41347  cdleme20m  41348  cdleme21ct  41354  cdleme22d  41368  cdleme22e  41369  cdleme22eALTN  41370  cdleme26e  41384  cdleme27a  41392  cdleme28a  41395  cdleme30a  41403  cdleme43fsv1snlem  41445  cdlemefs44  41451  cdlemefs45ee  41455  cdleme35sn2aw  41483  cdleme36a  41485  cdleme39n  41491  cdleme40m  41492  cdleme42k  41509  cdlemeg47rv2  41535  cdlemeg46frv  41550  cdlemeg46vrg  41552  cdlemeg46rgv  41553  cdlemeg46req  41554  cdlemg2fv2  41625  cdlemg4g  41641  cdlemg4  41642  cdlemg6c  41645  cdlemg8b  41653  cdlemg8c  41654  cdlemg9a  41657  cdlemg9b  41658  cdlemg9  41659  cdlemg12a  41668  cdlemg12b  41669  cdlemg12c  41670  cdlemg17h  41693  cdlemg18b  41704  cdlemg18c  41705  cdlemg31b0a  41720  cdlemg27b  41721  cdlemg31d  41725  cdlemg28b  41728  cdlemg33a  41731  cdlemg33b  41732  cdlemg33c  41733  cdlemg33d  41734  cdlemg33e  41735  cdlemg33  41736  cdlemh  41842  cdlemk6  41862  cdlemki  41866  cdlemksat  41871  cdlemksv2  41872  cdlemk7  41873  cdlemk11  41874  cdlemk12  41875  cdlemkole  41878  cdlemk14  41879  cdlemk15  41880  cdlemk17  41883  cdlemk1u  41884  cdlemk5u  41886  cdlemk6u  41887  cdlemk7u  41895  cdlemk11u  41896  cdlemk12u  41897  cdlemk7u-2N  41913  cdlemk11u-2N  41914  cdlemk12u-2N  41915  cdlemk20-2N  41917  cdlemk28-3  41933  cdlemk33N  41934  cdlemk34  41935  cdlemk37  41939  cdlemk39  41941  cdlemk35s  41962  cdlemk39s  41964  cdlemk47  41974  cdlemk48  41975  cdlemk50  41977  cdlemk51  41978  cdlemk52  41979  cdlemkyyN  41987  cdlemk43N  41988  cdlemn2  42220  cdlemn10  42231