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  8365  omeu  8569  expmordi  14202  hash7g  14522  4sqlem18  17021  vdwlem10  17049  0catg  17743  mvrf1  22103  mdetuni0  22746  mdetmul  22748  tsmsxp  24280  ax5seglem3  29221  btwnconn1lem1  36477  btwnconn1lem2  36478  btwnconn1lem3  36479  btwnconn1lem12  36488  btwnconn1lem13  36489  lshpkrlem6  39778  athgt  40119  2llnjN  40230  dalaw  40549  lhpmcvr4N  40689  cdlemb2  40704  4atexlemex6  40737  cdlemd7  40867  cdleme01N  40884  cdleme02N  40885  cdleme0ex1N  40886  cdleme0ex2N  40887  cdleme7aa  40905  cdleme7c  40908  cdleme7d  40909  cdleme7e  40910  cdleme7ga  40911  cdleme7  40912  cdleme11a  40923  cdleme20k  40982  cdleme27cl  41029  cdleme42e  41142  cdleme42h  41145  cdleme42i  41146  cdlemf  41226  cdlemg2kq  41265  cdlemg2m  41267  cdlemg8a  41290  cdlemg11aq  41301  cdlemg10c  41302  cdlemg11b  41305  cdlemg17a  41324  cdlemg31b0N  41357  cdlemg31c  41362  cdlemg33c0  41365  cdlemg41  41381  cdlemh2  41479  cdlemn9  41868  dihglbcpreN  41963  dihmeetlem3N  41968  dihmeetlem13N  41982  pellex  43453