Theorem simp22l 1384

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

Assertion

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

Proof of Theorem simp22l

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  ax5seglem6  26034  segconeu  32444  3atlem2  35266  lplncvrlvol2  35397  paddasslem15  35616  4atex  35858  trlval4  35970  cdlemc5  35977  cdlemc6  35978  cdlemd2  35981  cdlemd3  35982  cdlemd4  35983  cdleme0moN  36007  cdleme3g  36016  cdleme3h  36017  cdleme3  36019  cdleme11g  36047  cdleme11h  36048  cdleme11j  36049  cdleme11k  36050  cdleme11l  36051  cdleme11  36052  cdleme14  36055  cdleme15a  36056  cdleme15c  36058  cdleme15d  36059  cdleme15  36060  cdleme16b  36061  cdleme16c  36062  cdleme16d  36063  cdleme16e  36064  cdleme16f  36065  cdleme18a  36073  cdleme18b  36074  cdleme18c  36075  cdleme19b  36086  cdleme19e  36089  cdleme20bN  36092  cdleme20c  36093  cdleme20d  36094  cdleme20e  36095  cdleme20f  36096  cdleme20g  36097  cdleme20h  36098  cdleme20j  36100  cdleme20l2  36103  cdleme20l  36104  cdleme20m  36105  cdleme21ct  36111  cdleme22d  36125  cdleme22e  36126  cdleme22eALTN  36127  cdleme26e  36141  cdleme27a  36149  cdleme28a  36152  cdleme30a  36160  cdleme43fsv1snlem  36202  cdlemefs44  36208  cdlemefs45ee  36212  cdleme35sn2aw  36240  cdleme36a  36242  cdleme39n  36248  cdleme40m  36249  cdleme42k  36266  cdlemeg47rv2  36292  cdlemeg46frv  36307  cdlemeg46vrg  36309  cdlemeg46rgv  36310  cdlemeg46req  36311  cdlemg2fv2  36382  cdlemg4g  36398  cdlemg4  36399  cdlemg6c  36402  cdlemg8b  36410  cdlemg8c  36411  cdlemg9a  36414  cdlemg9b  36415  cdlemg9  36416  cdlemg12a  36425  cdlemg12b  36426  cdlemg12c  36427  cdlemg17h  36450  cdlemg18b  36461  cdlemg18c  36462  cdlemg31b0a  36477  cdlemg27b  36478  cdlemg31d  36482  cdlemg28b  36485  cdlemg33a  36488  cdlemg33b  36489  cdlemg33c  36490  cdlemg33d  36491  cdlemg33e  36492  cdlemg33  36493  cdlemh  36599  cdlemk6  36619  cdlemki  36623  cdlemksat  36628  cdlemksv2  36629  cdlemk7  36630  cdlemk11  36631  cdlemk12  36632  cdlemkole  36635  cdlemk14  36636  cdlemk15  36637  cdlemk17  36640  cdlemk1u  36641  cdlemk5u  36643  cdlemk6u  36644  cdlemk7u  36652  cdlemk11u  36653  cdlemk12u  36654  cdlemk7u-2N  36670  cdlemk11u-2N  36671  cdlemk12u-2N  36672  cdlemk20-2N  36674  cdlemk28-3  36690  cdlemk33N  36691  cdlemk34  36692  cdlemk37  36696  cdlemk39  36698  cdlemk35s  36719  cdlemk39s  36721  cdlemk47  36731  cdlemk48  36732  cdlemk50  36734  cdlemk51  36735  cdlemk52  36736  cdlemkyyN  36744  cdlemk43N  36745  cdlemn2  36977  cdlemn10  36988