Theorem simp2ll 1278

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

Assertion

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

Proof of Theorem simp2ll

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  tfrlem5  7759  omeu  7949  4sqlem18  16070  vdwlem10  16098  0catg  16733  mvrf1  19822  mdetuni0  20832  mdetmul  20834  tsmsxp  22366  ax5seglem3  26280  btwnconn1lem1  32783  btwnconn1lem2  32784  btwnconn1lem3  32785  btwnconn1lem12  32794  btwnconn1lem13  32795  lshpkrlem6  35271  athgt  35612  2llnjN  35723  dalaw  36042  lhpmcvr4N  36182  cdlemb2  36197  4atexlemex6  36230  cdlemd7  36360  cdleme01N  36377  cdleme02N  36378  cdleme0ex1N  36379  cdleme0ex2N  36380  cdleme7aa  36398  cdleme7c  36401  cdleme7d  36402  cdleme7e  36403  cdleme7ga  36404  cdleme7  36405  cdleme11a  36416  cdleme20k  36475  cdleme27cl  36522  cdleme42e  36635  cdleme42h  36638  cdleme42i  36639  cdlemf  36719  cdlemg2kq  36758  cdlemg2m  36760  cdlemg8a  36783  cdlemg11aq  36794  cdlemg10c  36795  cdlemg11b  36798  cdlemg17a  36817  cdlemg31b0N  36850  cdlemg31c  36855  cdlemg33c0  36858  cdlemg41  36874  cdlemh2  36972  cdlemn9  37361  dihglbcpreN  37456  dihmeetlem3N  37461  dihmeetlem13N  37475  pellex  38363  expmordi  38475