Theorem simp2ll 1307

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

Assertion

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

Proof of Theorem simp2ll

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  tfrlem5  7646  omeu  7836  4sqlem18  15888  vdwlem10  15916  0catg  16569  mvrf1  19647  mdetuni0  20649  mdetmul  20651  tsmsxp  22179  ax5seglem3  26031  btwnconn1lem1  32521  btwnconn1lem2  32522  btwnconn1lem3  32523  btwnconn1lem12  32532  btwnconn1lem13  32533  lshpkrlem6  34923  athgt  35263  2llnjN  35374  dalaw  35693  lhpmcvr4N  35833  cdlemb2  35848  4atexlemex6  35881  cdlemd7  36012  cdleme01N  36029  cdleme02N  36030  cdleme0ex1N  36031  cdleme0ex2N  36032  cdleme7aa  36050  cdleme7c  36053  cdleme7d  36054  cdleme7e  36055  cdleme7ga  36056  cdleme7  36057  cdleme11a  36068  cdleme20k  36127  cdleme27cl  36174  cdleme42e  36287  cdleme42h  36290  cdleme42i  36291  cdlemf  36371  cdlemg2kq  36410  cdlemg2m  36412  cdlemg8a  36435  cdlemg11aq  36446  cdlemg10c  36447  cdlemg11b  36450  cdlemg17a  36469  cdlemg31b0N  36502  cdlemg31c  36507  cdlemg33c0  36510  cdlemg41  36526  cdlemh2  36624  cdlemn9  37014  dihglbcpreN  37109  dihmeetlem3N  37114  dihmeetlem13N  37128  pellex  37919  expmordi  38032