Theorem simp2ll 1259

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

Assertion

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

Proof of Theorem simp2ll

Step	Hyp	Ref	Expression
1		simpll 779	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)
2	1	3ad2ant2 1152	1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  tfrlem5  8418  omeu  8624  expmordi  14340  hash7g  14661  4sqlem18  17172  vdwlem10  17200  0catg  17894  mvrf1  22326  mdetuni0  22969  mdetmul  22971  tsmsxp  24507  ax5seglem3  29542  btwnconn1lem1  37043  btwnconn1lem2  37044  btwnconn1lem3  37045  btwnconn1lem12  37054  btwnconn1lem13  37055  lshpkrlem6  40375  athgt  40716  2llnjN  40827  dalaw  41146  lhpmcvr4N  41286  cdlemb2  41301  4atexlemex6  41334  cdlemd7  41464  cdleme01N  41481  cdleme02N  41482  cdleme0ex1N  41483  cdleme0ex2N  41484  cdleme7aa  41502  cdleme7c  41505  cdleme7d  41506  cdleme7e  41507  cdleme7ga  41508  cdleme7  41509  cdleme11a  41520  cdleme20k  41579  cdleme27cl  41626  cdleme42e  41739  cdleme42h  41742  cdleme42i  41743  cdlemf  41823  cdlemg2kq  41862  cdlemg2m  41864  cdlemg8a  41887  cdlemg11aq  41898  cdlemg10c  41899  cdlemg11b  41902  cdlemg17a  41921  cdlemg31b0N  41954  cdlemg31c  41959  cdlemg33c0  41962  cdlemg41  41978  cdlemh2  42076  cdlemn9  42465  dihglbcpreN  42560  dihmeetlem3N  42565  dihmeetlem13N  42579  pellex  44046