Theorem simp2ll 1257

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

Assertion

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

Proof of Theorem simp2ll

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  tfrlem5  8354  omeu  8558  expmordi  14194  hash7g  14513  4sqlem18  17012  vdwlem10  17040  0catg  17734  mvrf1  22095  mdetuni0  22739  mdetmul  22741  tsmsxp  24273  ax5seglem3  29190  btwnconn1lem1  36450  btwnconn1lem2  36451  btwnconn1lem3  36452  btwnconn1lem12  36461  btwnconn1lem13  36462  lshpkrlem6  39751  athgt  40092  2llnjN  40203  dalaw  40522  lhpmcvr4N  40662  cdlemb2  40677  4atexlemex6  40710  cdlemd7  40840  cdleme01N  40857  cdleme02N  40858  cdleme0ex1N  40859  cdleme0ex2N  40860  cdleme7aa  40878  cdleme7c  40881  cdleme7d  40882  cdleme7e  40883  cdleme7ga  40884  cdleme7  40885  cdleme11a  40896  cdleme20k  40955  cdleme27cl  41002  cdleme42e  41115  cdleme42h  41118  cdleme42i  41119  cdlemf  41199  cdlemg2kq  41238  cdlemg2m  41240  cdlemg8a  41263  cdlemg11aq  41274  cdlemg10c  41275  cdlemg11b  41278  cdlemg17a  41297  cdlemg31b0N  41330  cdlemg31c  41335  cdlemg33c0  41338  cdlemg41  41354  cdlemh2  41452  cdlemn9  41841  dihglbcpreN  41936  dihmeetlem3N  41941  dihmeetlem13N  41955  pellex  43424