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  9635  ax5seglem6  29007  segconeu  36205  3atlem2  39740  lplncvrlvol2  39871  paddasslem15  40090  4atex  40332  trlval4  40444  cdlemc5  40451  cdlemc6  40452  cdlemd2  40455  cdlemd3  40456  cdlemd4  40457  cdleme0moN  40481  cdleme3g  40490  cdleme3h  40491  cdleme3  40493  cdleme11g  40521  cdleme11h  40522  cdleme11j  40523  cdleme11k  40524  cdleme11l  40525  cdleme11  40526  cdleme14  40529  cdleme15a  40530  cdleme15c  40532  cdleme15d  40533  cdleme15  40534  cdleme16b  40535  cdleme16c  40536  cdleme16d  40537  cdleme16e  40538  cdleme16f  40539  cdleme18a  40547  cdleme18b  40548  cdleme18c  40549  cdleme19b  40560  cdleme19e  40563  cdleme20bN  40566  cdleme20c  40567  cdleme20d  40568  cdleme20e  40569  cdleme20f  40570  cdleme20g  40571  cdleme20h  40572  cdleme20j  40574  cdleme20l2  40577  cdleme20l  40578  cdleme20m  40579  cdleme21ct  40585  cdleme22d  40599  cdleme22e  40600  cdleme22eALTN  40601  cdleme26e  40615  cdleme27a  40623  cdleme28a  40626  cdleme30a  40634  cdleme43fsv1snlem  40676  cdlemefs44  40682  cdlemefs45ee  40686  cdleme35sn2aw  40714  cdleme36a  40716  cdleme39n  40722  cdleme40m  40723  cdleme42k  40740  cdlemeg47rv2  40766  cdlemeg46frv  40781  cdlemeg46vrg  40783  cdlemeg46rgv  40784  cdlemeg46req  40785  cdlemg2fv2  40856  cdlemg4g  40872  cdlemg4  40873  cdlemg6c  40876  cdlemg8b  40884  cdlemg8c  40885  cdlemg9a  40888  cdlemg9b  40889  cdlemg9  40890  cdlemg12a  40899  cdlemg12b  40900  cdlemg12c  40901  cdlemg17h  40924  cdlemg18b  40935  cdlemg18c  40936  cdlemg31b0a  40951  cdlemg27b  40952  cdlemg31d  40956  cdlemg28b  40959  cdlemg33a  40962  cdlemg33b  40963  cdlemg33c  40964  cdlemg33d  40965  cdlemg33e  40966  cdlemg33  40967  cdlemh  41073  cdlemk6  41093  cdlemki  41097  cdlemksat  41102  cdlemksv2  41103  cdlemk7  41104  cdlemk11  41105  cdlemk12  41106  cdlemkole  41109  cdlemk14  41110  cdlemk15  41111  cdlemk17  41114  cdlemk1u  41115  cdlemk5u  41117  cdlemk6u  41118  cdlemk7u  41126  cdlemk11u  41127  cdlemk12u  41128  cdlemk7u-2N  41144  cdlemk11u-2N  41145  cdlemk12u-2N  41146  cdlemk20-2N  41148  cdlemk28-3  41164  cdlemk33N  41165  cdlemk34  41166  cdlemk37  41170  cdlemk39  41172  cdlemk35s  41193  cdlemk39s  41195  cdlemk47  41205  cdlemk48  41206  cdlemk50  41208  cdlemk51  41209  cdlemk52  41210  cdlemkyyN  41218  cdlemk43N  41219  cdlemn2  41451  cdlemn10  41462