Theorem simp22l 1173

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

Assertion

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

Proof of Theorem simp22l

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  ax5seglem6  25614  segconeu  31288  3atlem2  33788  lplncvrlvol2  33919  paddasslem15  34138  4atex  34380  trlval4  34493  cdlemc5  34500  cdlemc6  34501  cdlemd2  34504  cdlemd3  34505  cdlemd4  34506  cdleme0moN  34530  cdleme3g  34539  cdleme3h  34540  cdleme3  34542  cdleme11g  34570  cdleme11h  34571  cdleme11j  34572  cdleme11k  34573  cdleme11l  34574  cdleme11  34575  cdleme14  34578  cdleme15a  34579  cdleme15c  34581  cdleme15d  34582  cdleme15  34583  cdleme16b  34584  cdleme16c  34585  cdleme16d  34586  cdleme16e  34587  cdleme16f  34588  cdleme18a  34596  cdleme18b  34597  cdleme18c  34598  cdleme19b  34610  cdleme19e  34613  cdleme20bN  34616  cdleme20c  34617  cdleme20d  34618  cdleme20e  34619  cdleme20f  34620  cdleme20g  34621  cdleme20h  34622  cdleme20j  34624  cdleme20l2  34627  cdleme20l  34628  cdleme20m  34629  cdleme21ct  34635  cdleme22d  34649  cdleme22e  34650  cdleme22eALTN  34651  cdleme26e  34665  cdleme27a  34673  cdleme28a  34676  cdleme30a  34684  cdleme43fsv1snlem  34726  cdlemefs44  34732  cdlemefs45ee  34736  cdleme35sn2aw  34764  cdleme36a  34766  cdleme39n  34772  cdleme40m  34773  cdleme42k  34790  cdlemeg47rv2  34816  cdlemeg46frv  34831  cdlemeg46vrg  34833  cdlemeg46rgv  34834  cdlemeg46req  34835  cdlemg2fv2  34906  cdlemg4g  34922  cdlemg4  34923  cdlemg6c  34926  cdlemg8b  34934  cdlemg8c  34935  cdlemg9a  34938  cdlemg9b  34939  cdlemg9  34940  cdlemg12a  34949  cdlemg12b  34950  cdlemg12c  34951  cdlemg17h  34974  cdlemg18b  34985  cdlemg18c  34986  cdlemg31b0a  35001  cdlemg27b  35002  cdlemg31d  35006  cdlemg28b  35009  cdlemg33a  35012  cdlemg33b  35013  cdlemg33c  35014  cdlemg33d  35015  cdlemg33e  35016  cdlemg33  35017  cdlemh  35123  cdlemk6  35143  cdlemki  35147  cdlemksat  35152  cdlemksv2  35153  cdlemk7  35154  cdlemk11  35155  cdlemk12  35156  cdlemkole  35159  cdlemk14  35160  cdlemk15  35161  cdlemk17  35164  cdlemk1u  35165  cdlemk5u  35167  cdlemk6u  35168  cdlemk7u  35176  cdlemk11u  35177  cdlemk12u  35178  cdlemk7u-2N  35194  cdlemk11u-2N  35195  cdlemk12u-2N  35196  cdlemk20-2N  35198  cdlemk28-3  35214  cdlemk33N  35215  cdlemk34  35216  cdlemk37  35220  cdlemk39  35222  cdlemk35s  35243  cdlemk39s  35245  cdlemk47  35255  cdlemk48  35256  cdlemk50  35258  cdlemk51  35259  cdlemk52  35260  cdlemkyyN  35268  cdlemk43N  35269  cdlemn2  35502  cdlemn10  35513