Theorem simp21l 1291

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

Assertion

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

Proof of Theorem simp21l

Step	Hyp	Ref	Expression
1		simp1l 1198	. 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:  modexp  14145  segconeu  36051  4atlem10  39651  lplncvrlvol2  39660  4atex  40121  4atex2-0cOLDN  40125  cdlemd2  40244  cdlemd3  40245  cdlemd4  40246  cdleme0e  40262  cdleme0moN  40270  cdleme3g  40279  cdleme3h  40280  cdleme3  40282  cdleme9  40298  cdleme11c  40306  cdleme11dN  40307  cdleme11e  40308  cdleme11fN  40309  cdleme11h  40311  cdleme11j  40312  cdleme11k  40313  cdleme11  40315  cdleme12  40316  cdleme13  40317  cdleme14  40318  cdleme15a  40319  cdleme15b  40320  cdleme15c  40321  cdleme15d  40322  cdleme15  40323  cdleme16b  40324  cdleme16c  40325  cdleme16d  40326  cdleme16e  40327  cdleme16f  40328  cdleme17d1  40334  cdleme18a  40336  cdleme18b  40337  cdleme18c  40338  cdleme18d  40340  cdleme19b  40349  cdleme19d  40351  cdleme19e  40352  cdleme20c  40356  cdleme20d  40357  cdleme20e  40358  cdleme20f  40359  cdleme20g  40360  cdleme20h  40361  cdleme20j  40363  cdleme20l2  40366  cdleme20l  40367  cdleme20m  40368  cdleme20  40369  cdleme21ct  40374  cdleme21e  40376  cdleme21i  40380  cdleme22aa  40384  cdleme22cN  40387  cdleme22d  40388  cdleme22e  40389  cdleme22eALTN  40390  cdleme22f  40391  cdleme26e  40404  cdleme27a  40412  cdleme32e  40490  cdlemg2fv2  40645  cdlemg4a  40653  cdlemg4d  40658  cdlemg4  40662  cdlemg6c  40665  cdlemg8b  40673  cdlemg8c  40674  cdlemg9a  40677  cdlemg9  40679  cdlemg12a  40688  cdlemg12c  40690  cdlemg17dALTN  40709  cdlemg17h  40713  cdlemg18b  40724  cdlemg18c  40725  cdlemg18d  40726  cdlemg18  40727  cdlemg19a  40728  cdlemg21  40731  cdlemg28a  40738  cdlemg31b0a  40740  cdlemg31d  40745  cdlemg33b0  40746  cdlemg33a  40751  cdlemh  40862  cdlemk5  40881  cdlemk6  40882  cdlemk7  40893  cdlemk11  40894  cdlemk12  40895  cdlemk21N  40918  cdlemk20  40919  cdlemk28-3  40953  cdlemk34  40955  cdlemkfid3N  40970  cdlemk35s-id  40983  cdlemk39s-id  40985  cdlemk55u1  41010  cdlemn2  41240  cdlemn10  41251  dihjustlem  41261