Theorem simp22l 1309

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

Assertion

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

Proof of Theorem simp22l

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  ttrclselem2  9683  ax5seglem6  29193  segconeu  36374  3atlem2  40120  lplncvrlvol2  40251  paddasslem15  40470  4atex  40712  trlval4  40824  cdlemc5  40831  cdlemc6  40832  cdlemd2  40835  cdlemd3  40836  cdlemd4  40837  cdleme0moN  40861  cdleme3g  40870  cdleme3h  40871  cdleme3  40873  cdleme11g  40901  cdleme11h  40902  cdleme11j  40903  cdleme11k  40904  cdleme11l  40905  cdleme11  40906  cdleme14  40909  cdleme15a  40910  cdleme15c  40912  cdleme15d  40913  cdleme15  40914  cdleme16b  40915  cdleme16c  40916  cdleme16d  40917  cdleme16e  40918  cdleme16f  40919  cdleme18a  40927  cdleme18b  40928  cdleme18c  40929  cdleme19b  40940  cdleme19e  40943  cdleme20bN  40946  cdleme20c  40947  cdleme20d  40948  cdleme20e  40949  cdleme20f  40950  cdleme20g  40951  cdleme20h  40952  cdleme20j  40954  cdleme20l2  40957  cdleme20l  40958  cdleme20m  40959  cdleme21ct  40965  cdleme22d  40979  cdleme22e  40980  cdleme22eALTN  40981  cdleme26e  40995  cdleme27a  41003  cdleme28a  41006  cdleme30a  41014  cdleme43fsv1snlem  41056  cdlemefs44  41062  cdlemefs45ee  41066  cdleme35sn2aw  41094  cdleme36a  41096  cdleme39n  41102  cdleme40m  41103  cdleme42k  41120  cdlemeg47rv2  41146  cdlemeg46frv  41161  cdlemeg46vrg  41163  cdlemeg46rgv  41164  cdlemeg46req  41165  cdlemg2fv2  41236  cdlemg4g  41252  cdlemg4  41253  cdlemg6c  41256  cdlemg8b  41264  cdlemg8c  41265  cdlemg9a  41268  cdlemg9b  41269  cdlemg9  41270  cdlemg12a  41279  cdlemg12b  41280  cdlemg12c  41281  cdlemg17h  41304  cdlemg18b  41315  cdlemg18c  41316  cdlemg31b0a  41331  cdlemg27b  41332  cdlemg31d  41336  cdlemg28b  41339  cdlemg33a  41342  cdlemg33b  41343  cdlemg33c  41344  cdlemg33d  41345  cdlemg33e  41346  cdlemg33  41347  cdlemh  41453  cdlemk6  41473  cdlemki  41477  cdlemksat  41482  cdlemksv2  41483  cdlemk7  41484  cdlemk11  41485  cdlemk12  41486  cdlemkole  41489  cdlemk14  41490  cdlemk15  41491  cdlemk17  41494  cdlemk1u  41495  cdlemk5u  41497  cdlemk6u  41498  cdlemk7u  41506  cdlemk11u  41507  cdlemk12u  41508  cdlemk7u-2N  41524  cdlemk11u-2N  41525  cdlemk12u-2N  41526  cdlemk20-2N  41528  cdlemk28-3  41544  cdlemk33N  41545  cdlemk34  41546  cdlemk37  41550  cdlemk39  41552  cdlemk35s  41573  cdlemk39s  41575  cdlemk47  41585  cdlemk48  41586  cdlemk50  41588  cdlemk51  41589  cdlemk52  41590  cdlemkyyN  41598  cdlemk43N  41599  cdlemn2  41831  cdlemn10  41842