Theorem simp2ll 1238

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 1132	1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  tfrlem5  8401  omeu  8606  expmordi  14164  4sqlem18  16931  vdwlem10  16959  0catg  17668  mvrf1  21928  mdetuni0  22536  mdetmul  22538  tsmsxp  24072  ax5seglem3  28755  btwnconn1lem1  35683  btwnconn1lem2  35684  btwnconn1lem3  35685  btwnconn1lem12  35694  btwnconn1lem13  35695  lshpkrlem6  38587  athgt  38929  2llnjN  39040  dalaw  39359  lhpmcvr4N  39499  cdlemb2  39514  4atexlemex6  39547  cdlemd7  39677  cdleme01N  39694  cdleme02N  39695  cdleme0ex1N  39696  cdleme0ex2N  39697  cdleme7aa  39715  cdleme7c  39718  cdleme7d  39719  cdleme7e  39720  cdleme7ga  39721  cdleme7  39722  cdleme11a  39733  cdleme20k  39792  cdleme27cl  39839  cdleme42e  39952  cdleme42h  39955  cdleme42i  39956  cdlemf  40036  cdlemg2kq  40075  cdlemg2m  40077  cdlemg8a  40100  cdlemg11aq  40111  cdlemg10c  40112  cdlemg11b  40115  cdlemg17a  40134  cdlemg31b0N  40167  cdlemg31c  40172  cdlemg33c0  40175  cdlemg41  40191  cdlemh2  40289  cdlemn9  40678  dihglbcpreN  40773  dihmeetlem3N  40778  dihmeetlem13N  40792  pellex  42255