Theorem simp22l 1293

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

Assertion

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

Proof of Theorem simp22l

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

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

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 1088

This theorem is referenced by:  ttrclselem2  9686  ax5seglem6  28868  segconeu  36006  3atlem2  39485  lplncvrlvol2  39616  paddasslem15  39835  4atex  40077  trlval4  40189  cdlemc5  40196  cdlemc6  40197  cdlemd2  40200  cdlemd3  40201  cdlemd4  40202  cdleme0moN  40226  cdleme3g  40235  cdleme3h  40236  cdleme3  40238  cdleme11g  40266  cdleme11h  40267  cdleme11j  40268  cdleme11k  40269  cdleme11l  40270  cdleme11  40271  cdleme14  40274  cdleme15a  40275  cdleme15c  40277  cdleme15d  40278  cdleme15  40279  cdleme16b  40280  cdleme16c  40281  cdleme16d  40282  cdleme16e  40283  cdleme16f  40284  cdleme18a  40292  cdleme18b  40293  cdleme18c  40294  cdleme19b  40305  cdleme19e  40308  cdleme20bN  40311  cdleme20c  40312  cdleme20d  40313  cdleme20e  40314  cdleme20f  40315  cdleme20g  40316  cdleme20h  40317  cdleme20j  40319  cdleme20l2  40322  cdleme20l  40323  cdleme20m  40324  cdleme21ct  40330  cdleme22d  40344  cdleme22e  40345  cdleme22eALTN  40346  cdleme26e  40360  cdleme27a  40368  cdleme28a  40371  cdleme30a  40379  cdleme43fsv1snlem  40421  cdlemefs44  40427  cdlemefs45ee  40431  cdleme35sn2aw  40459  cdleme36a  40461  cdleme39n  40467  cdleme40m  40468  cdleme42k  40485  cdlemeg47rv2  40511  cdlemeg46frv  40526  cdlemeg46vrg  40528  cdlemeg46rgv  40529  cdlemeg46req  40530  cdlemg2fv2  40601  cdlemg4g  40617  cdlemg4  40618  cdlemg6c  40621  cdlemg8b  40629  cdlemg8c  40630  cdlemg9a  40633  cdlemg9b  40634  cdlemg9  40635  cdlemg12a  40644  cdlemg12b  40645  cdlemg12c  40646  cdlemg17h  40669  cdlemg18b  40680  cdlemg18c  40681  cdlemg31b0a  40696  cdlemg27b  40697  cdlemg31d  40701  cdlemg28b  40704  cdlemg33a  40707  cdlemg33b  40708  cdlemg33c  40709  cdlemg33d  40710  cdlemg33e  40711  cdlemg33  40712  cdlemh  40818  cdlemk6  40838  cdlemki  40842  cdlemksat  40847  cdlemksv2  40848  cdlemk7  40849  cdlemk11  40850  cdlemk12  40851  cdlemkole  40854  cdlemk14  40855  cdlemk15  40856  cdlemk17  40859  cdlemk1u  40860  cdlemk5u  40862  cdlemk6u  40863  cdlemk7u  40871  cdlemk11u  40872  cdlemk12u  40873  cdlemk7u-2N  40889  cdlemk11u-2N  40890  cdlemk12u-2N  40891  cdlemk20-2N  40893  cdlemk28-3  40909  cdlemk33N  40910  cdlemk34  40911  cdlemk37  40915  cdlemk39  40917  cdlemk35s  40938  cdlemk39s  40940  cdlemk47  40950  cdlemk48  40951  cdlemk50  40953  cdlemk51  40954  cdlemk52  40955  cdlemkyyN  40963  cdlemk43N  40964  cdlemn2  41196  cdlemn10  41207