Theorem simp2ll 1253

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

Assertion

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

Proof of Theorem simp2ll

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  tfrlem5  8345  omeu  8549  expmordi  14177  hash7g  14496  4sqlem18  16981  vdwlem10  17009  0catg  17703  mvrf1  22017  mdetuni0  22661  mdetmul  22663  tsmsxp  24195  ax5seglem3  29078  btwnconn1lem1  36401  btwnconn1lem2  36402  btwnconn1lem3  36403  btwnconn1lem12  36412  btwnconn1lem13  36413  lshpkrlem6  39703  athgt  40044  2llnjN  40155  dalaw  40474  lhpmcvr4N  40614  cdlemb2  40629  4atexlemex6  40662  cdlemd7  40792  cdleme01N  40809  cdleme02N  40810  cdleme0ex1N  40811  cdleme0ex2N  40812  cdleme7aa  40830  cdleme7c  40833  cdleme7d  40834  cdleme7e  40835  cdleme7ga  40836  cdleme7  40837  cdleme11a  40848  cdleme20k  40907  cdleme27cl  40954  cdleme42e  41067  cdleme42h  41070  cdleme42i  41071  cdlemf  41151  cdlemg2kq  41190  cdlemg2m  41192  cdlemg8a  41215  cdlemg11aq  41226  cdlemg10c  41227  cdlemg11b  41230  cdlemg17a  41249  cdlemg31b0N  41282  cdlemg31c  41287  cdlemg33c0  41290  cdlemg41  41306  cdlemh2  41404  cdlemn9  41793  dihglbcpreN  41888  dihmeetlem3N  41893  dihmeetlem13N  41907  pellex  43376