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  9641  ax5seglem6  28897  segconeu  35984  3atlem2  39463  lplncvrlvol2  39594  paddasslem15  39813  4atex  40055  trlval4  40167  cdlemc5  40174  cdlemc6  40175  cdlemd2  40178  cdlemd3  40179  cdlemd4  40180  cdleme0moN  40204  cdleme3g  40213  cdleme3h  40214  cdleme3  40216  cdleme11g  40244  cdleme11h  40245  cdleme11j  40246  cdleme11k  40247  cdleme11l  40248  cdleme11  40249  cdleme14  40252  cdleme15a  40253  cdleme15c  40255  cdleme15d  40256  cdleme15  40257  cdleme16b  40258  cdleme16c  40259  cdleme16d  40260  cdleme16e  40261  cdleme16f  40262  cdleme18a  40270  cdleme18b  40271  cdleme18c  40272  cdleme19b  40283  cdleme19e  40286  cdleme20bN  40289  cdleme20c  40290  cdleme20d  40291  cdleme20e  40292  cdleme20f  40293  cdleme20g  40294  cdleme20h  40295  cdleme20j  40297  cdleme20l2  40300  cdleme20l  40301  cdleme20m  40302  cdleme21ct  40308  cdleme22d  40322  cdleme22e  40323  cdleme22eALTN  40324  cdleme26e  40338  cdleme27a  40346  cdleme28a  40349  cdleme30a  40357  cdleme43fsv1snlem  40399  cdlemefs44  40405  cdlemefs45ee  40409  cdleme35sn2aw  40437  cdleme36a  40439  cdleme39n  40445  cdleme40m  40446  cdleme42k  40463  cdlemeg47rv2  40489  cdlemeg46frv  40504  cdlemeg46vrg  40506  cdlemeg46rgv  40507  cdlemeg46req  40508  cdlemg2fv2  40579  cdlemg4g  40595  cdlemg4  40596  cdlemg6c  40599  cdlemg8b  40607  cdlemg8c  40608  cdlemg9a  40611  cdlemg9b  40612  cdlemg9  40613  cdlemg12a  40622  cdlemg12b  40623  cdlemg12c  40624  cdlemg17h  40647  cdlemg18b  40658  cdlemg18c  40659  cdlemg31b0a  40674  cdlemg27b  40675  cdlemg31d  40679  cdlemg28b  40682  cdlemg33a  40685  cdlemg33b  40686  cdlemg33c  40687  cdlemg33d  40688  cdlemg33e  40689  cdlemg33  40690  cdlemh  40796  cdlemk6  40816  cdlemki  40820  cdlemksat  40825  cdlemksv2  40826  cdlemk7  40827  cdlemk11  40828  cdlemk12  40829  cdlemkole  40832  cdlemk14  40833  cdlemk15  40834  cdlemk17  40837  cdlemk1u  40838  cdlemk5u  40840  cdlemk6u  40841  cdlemk7u  40849  cdlemk11u  40850  cdlemk12u  40851  cdlemk7u-2N  40867  cdlemk11u-2N  40868  cdlemk12u-2N  40869  cdlemk20-2N  40871  cdlemk28-3  40887  cdlemk33N  40888  cdlemk34  40889  cdlemk37  40893  cdlemk39  40895  cdlemk35s  40916  cdlemk39s  40918  cdlemk47  40928  cdlemk48  40929  cdlemk50  40931  cdlemk51  40932  cdlemk52  40933  cdlemkyyN  40941  cdlemk43N  40942  cdlemn2  41174  cdlemn10  41185