Theorem simp22l 1289

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

Assertion

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

Proof of Theorem simp22l

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  ttrclselem2  9769  ax5seglem6  28868  segconeu  35835  3atlem2  39183  lplncvrlvol2  39314  paddasslem15  39533  4atex  39775  trlval4  39887  cdlemc5  39894  cdlemc6  39895  cdlemd2  39898  cdlemd3  39899  cdlemd4  39900  cdleme0moN  39924  cdleme3g  39933  cdleme3h  39934  cdleme3  39936  cdleme11g  39964  cdleme11h  39965  cdleme11j  39966  cdleme11k  39967  cdleme11l  39968  cdleme11  39969  cdleme14  39972  cdleme15a  39973  cdleme15c  39975  cdleme15d  39976  cdleme15  39977  cdleme16b  39978  cdleme16c  39979  cdleme16d  39980  cdleme16e  39981  cdleme16f  39982  cdleme18a  39990  cdleme18b  39991  cdleme18c  39992  cdleme19b  40003  cdleme19e  40006  cdleme20bN  40009  cdleme20c  40010  cdleme20d  40011  cdleme20e  40012  cdleme20f  40013  cdleme20g  40014  cdleme20h  40015  cdleme20j  40017  cdleme20l2  40020  cdleme20l  40021  cdleme20m  40022  cdleme21ct  40028  cdleme22d  40042  cdleme22e  40043  cdleme22eALTN  40044  cdleme26e  40058  cdleme27a  40066  cdleme28a  40069  cdleme30a  40077  cdleme43fsv1snlem  40119  cdlemefs44  40125  cdlemefs45ee  40129  cdleme35sn2aw  40157  cdleme36a  40159  cdleme39n  40165  cdleme40m  40166  cdleme42k  40183  cdlemeg47rv2  40209  cdlemeg46frv  40224  cdlemeg46vrg  40226  cdlemeg46rgv  40227  cdlemeg46req  40228  cdlemg2fv2  40299  cdlemg4g  40315  cdlemg4  40316  cdlemg6c  40319  cdlemg8b  40327  cdlemg8c  40328  cdlemg9a  40331  cdlemg9b  40332  cdlemg9  40333  cdlemg12a  40342  cdlemg12b  40343  cdlemg12c  40344  cdlemg17h  40367  cdlemg18b  40378  cdlemg18c  40379  cdlemg31b0a  40394  cdlemg27b  40395  cdlemg31d  40399  cdlemg28b  40402  cdlemg33a  40405  cdlemg33b  40406  cdlemg33c  40407  cdlemg33d  40408  cdlemg33e  40409  cdlemg33  40410  cdlemh  40516  cdlemk6  40536  cdlemki  40540  cdlemksat  40545  cdlemksv2  40546  cdlemk7  40547  cdlemk11  40548  cdlemk12  40549  cdlemkole  40552  cdlemk14  40553  cdlemk15  40554  cdlemk17  40557  cdlemk1u  40558  cdlemk5u  40560  cdlemk6u  40561  cdlemk7u  40569  cdlemk11u  40570  cdlemk12u  40571  cdlemk7u-2N  40587  cdlemk11u-2N  40588  cdlemk12u-2N  40589  cdlemk20-2N  40591  cdlemk28-3  40607  cdlemk33N  40608  cdlemk34  40609  cdlemk37  40613  cdlemk39  40615  cdlemk35s  40636  cdlemk39s  40638  cdlemk47  40648  cdlemk48  40649  cdlemk50  40651  cdlemk51  40652  cdlemk52  40653  cdlemkyyN  40661  cdlemk43N  40662  cdlemn2  40894  cdlemn10  40905