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  9622  ax5seglem6  28919  segconeu  36062  3atlem2  39589  lplncvrlvol2  39720  paddasslem15  39939  4atex  40181  trlval4  40293  cdlemc5  40300  cdlemc6  40301  cdlemd2  40304  cdlemd3  40305  cdlemd4  40306  cdleme0moN  40330  cdleme3g  40339  cdleme3h  40340  cdleme3  40342  cdleme11g  40370  cdleme11h  40371  cdleme11j  40372  cdleme11k  40373  cdleme11l  40374  cdleme11  40375  cdleme14  40378  cdleme15a  40379  cdleme15c  40381  cdleme15d  40382  cdleme15  40383  cdleme16b  40384  cdleme16c  40385  cdleme16d  40386  cdleme16e  40387  cdleme16f  40388  cdleme18a  40396  cdleme18b  40397  cdleme18c  40398  cdleme19b  40409  cdleme19e  40412  cdleme20bN  40415  cdleme20c  40416  cdleme20d  40417  cdleme20e  40418  cdleme20f  40419  cdleme20g  40420  cdleme20h  40421  cdleme20j  40423  cdleme20l2  40426  cdleme20l  40427  cdleme20m  40428  cdleme21ct  40434  cdleme22d  40448  cdleme22e  40449  cdleme22eALTN  40450  cdleme26e  40464  cdleme27a  40472  cdleme28a  40475  cdleme30a  40483  cdleme43fsv1snlem  40525  cdlemefs44  40531  cdlemefs45ee  40535  cdleme35sn2aw  40563  cdleme36a  40565  cdleme39n  40571  cdleme40m  40572  cdleme42k  40589  cdlemeg47rv2  40615  cdlemeg46frv  40630  cdlemeg46vrg  40632  cdlemeg46rgv  40633  cdlemeg46req  40634  cdlemg2fv2  40705  cdlemg4g  40721  cdlemg4  40722  cdlemg6c  40725  cdlemg8b  40733  cdlemg8c  40734  cdlemg9a  40737  cdlemg9b  40738  cdlemg9  40739  cdlemg12a  40748  cdlemg12b  40749  cdlemg12c  40750  cdlemg17h  40773  cdlemg18b  40784  cdlemg18c  40785  cdlemg31b0a  40800  cdlemg27b  40801  cdlemg31d  40805  cdlemg28b  40808  cdlemg33a  40811  cdlemg33b  40812  cdlemg33c  40813  cdlemg33d  40814  cdlemg33e  40815  cdlemg33  40816  cdlemh  40922  cdlemk6  40942  cdlemki  40946  cdlemksat  40951  cdlemksv2  40952  cdlemk7  40953  cdlemk11  40954  cdlemk12  40955  cdlemkole  40958  cdlemk14  40959  cdlemk15  40960  cdlemk17  40963  cdlemk1u  40964  cdlemk5u  40966  cdlemk6u  40967  cdlemk7u  40975  cdlemk11u  40976  cdlemk12u  40977  cdlemk7u-2N  40993  cdlemk11u-2N  40994  cdlemk12u-2N  40995  cdlemk20-2N  40997  cdlemk28-3  41013  cdlemk33N  41014  cdlemk34  41015  cdlemk37  41019  cdlemk39  41021  cdlemk35s  41042  cdlemk39s  41044  cdlemk47  41054  cdlemk48  41055  cdlemk50  41057  cdlemk51  41058  cdlemk52  41059  cdlemkyyN  41067  cdlemk43N  41068  cdlemn2  41300  cdlemn10  41311