Theorem simp2ll 1241

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

Assertion

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

Proof of Theorem simp2ll

Step	Hyp	Ref	Expression
1		simpll 766	. 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:  tfrlem5  8351  omeu  8552  expmordi  14139  hash7g  14458  4sqlem18  16940  vdwlem10  16968  0catg  17656  mvrf1  21902  mdetuni0  22515  mdetmul  22517  tsmsxp  24049  ax5seglem3  28865  btwnconn1lem1  36082  btwnconn1lem2  36083  btwnconn1lem3  36084  btwnconn1lem12  36093  btwnconn1lem13  36094  lshpkrlem6  39115  athgt  39457  2llnjN  39568  dalaw  39887  lhpmcvr4N  40027  cdlemb2  40042  4atexlemex6  40075  cdlemd7  40205  cdleme01N  40222  cdleme02N  40223  cdleme0ex1N  40224  cdleme0ex2N  40225  cdleme7aa  40243  cdleme7c  40246  cdleme7d  40247  cdleme7e  40248  cdleme7ga  40249  cdleme7  40250  cdleme11a  40261  cdleme20k  40320  cdleme27cl  40367  cdleme42e  40480  cdleme42h  40483  cdleme42i  40484  cdlemf  40564  cdlemg2kq  40603  cdlemg2m  40605  cdlemg8a  40628  cdlemg11aq  40639  cdlemg10c  40640  cdlemg11b  40643  cdlemg17a  40662  cdlemg31b0N  40695  cdlemg31c  40700  cdlemg33c0  40703  cdlemg41  40719  cdlemh2  40817  cdlemn9  41206  dihglbcpreN  41301  dihmeetlem3N  41306  dihmeetlem13N  41320  pellex  42830