Theorem simp2ll 1238

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

Assertion

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

Proof of Theorem simp2ll

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  tfrlem5  8382  omeu  8587  expmordi  14136  4sqlem18  16899  vdwlem10  16927  0catg  17636  mvrf1  21764  mdetuni0  22343  mdetmul  22345  tsmsxp  23879  ax5seglem3  28456  btwnconn1lem1  35363  btwnconn1lem2  35364  btwnconn1lem3  35365  btwnconn1lem12  35374  btwnconn1lem13  35375  lshpkrlem6  38288  athgt  38630  2llnjN  38741  dalaw  39060  lhpmcvr4N  39200  cdlemb2  39215  4atexlemex6  39248  cdlemd7  39378  cdleme01N  39395  cdleme02N  39396  cdleme0ex1N  39397  cdleme0ex2N  39398  cdleme7aa  39416  cdleme7c  39419  cdleme7d  39420  cdleme7e  39421  cdleme7ga  39422  cdleme7  39423  cdleme11a  39434  cdleme20k  39493  cdleme27cl  39540  cdleme42e  39653  cdleme42h  39656  cdleme42i  39657  cdlemf  39737  cdlemg2kq  39776  cdlemg2m  39778  cdlemg8a  39801  cdlemg11aq  39812  cdlemg10c  39813  cdlemg11b  39816  cdlemg17a  39835  cdlemg31b0N  39868  cdlemg31c  39873  cdlemg33c0  39876  cdlemg41  39892  cdlemh2  39990  cdlemn9  40379  dihglbcpreN  40474  dihmeetlem3N  40479  dihmeetlem13N  40493  pellex  41875