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  9616  ax5seglem6  28910  segconeu  36044  3atlem2  39522  lplncvrlvol2  39653  paddasslem15  39872  4atex  40114  trlval4  40226  cdlemc5  40233  cdlemc6  40234  cdlemd2  40237  cdlemd3  40238  cdlemd4  40239  cdleme0moN  40263  cdleme3g  40272  cdleme3h  40273  cdleme3  40275  cdleme11g  40303  cdleme11h  40304  cdleme11j  40305  cdleme11k  40306  cdleme11l  40307  cdleme11  40308  cdleme14  40311  cdleme15a  40312  cdleme15c  40314  cdleme15d  40315  cdleme15  40316  cdleme16b  40317  cdleme16c  40318  cdleme16d  40319  cdleme16e  40320  cdleme16f  40321  cdleme18a  40329  cdleme18b  40330  cdleme18c  40331  cdleme19b  40342  cdleme19e  40345  cdleme20bN  40348  cdleme20c  40349  cdleme20d  40350  cdleme20e  40351  cdleme20f  40352  cdleme20g  40353  cdleme20h  40354  cdleme20j  40356  cdleme20l2  40359  cdleme20l  40360  cdleme20m  40361  cdleme21ct  40367  cdleme22d  40381  cdleme22e  40382  cdleme22eALTN  40383  cdleme26e  40397  cdleme27a  40405  cdleme28a  40408  cdleme30a  40416  cdleme43fsv1snlem  40458  cdlemefs44  40464  cdlemefs45ee  40468  cdleme35sn2aw  40496  cdleme36a  40498  cdleme39n  40504  cdleme40m  40505  cdleme42k  40522  cdlemeg47rv2  40548  cdlemeg46frv  40563  cdlemeg46vrg  40565  cdlemeg46rgv  40566  cdlemeg46req  40567  cdlemg2fv2  40638  cdlemg4g  40654  cdlemg4  40655  cdlemg6c  40658  cdlemg8b  40666  cdlemg8c  40667  cdlemg9a  40670  cdlemg9b  40671  cdlemg9  40672  cdlemg12a  40681  cdlemg12b  40682  cdlemg12c  40683  cdlemg17h  40706  cdlemg18b  40717  cdlemg18c  40718  cdlemg31b0a  40733  cdlemg27b  40734  cdlemg31d  40738  cdlemg28b  40741  cdlemg33a  40744  cdlemg33b  40745  cdlemg33c  40746  cdlemg33d  40747  cdlemg33e  40748  cdlemg33  40749  cdlemh  40855  cdlemk6  40875  cdlemki  40879  cdlemksat  40884  cdlemksv2  40885  cdlemk7  40886  cdlemk11  40887  cdlemk12  40888  cdlemkole  40891  cdlemk14  40892  cdlemk15  40893  cdlemk17  40896  cdlemk1u  40897  cdlemk5u  40899  cdlemk6u  40900  cdlemk7u  40908  cdlemk11u  40909  cdlemk12u  40910  cdlemk7u-2N  40926  cdlemk11u-2N  40927  cdlemk12u-2N  40928  cdlemk20-2N  40930  cdlemk28-3  40946  cdlemk33N  40947  cdlemk34  40948  cdlemk37  40952  cdlemk39  40954  cdlemk35s  40975  cdlemk39s  40977  cdlemk47  40987  cdlemk48  40988  cdlemk50  40990  cdlemk51  40991  cdlemk52  40992  cdlemkyyN  41000  cdlemk43N  41001  cdlemn2  41233  cdlemn10  41244