Theorem simp2ll 1259

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

Assertion

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

Proof of Theorem simp2ll

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  tfrlem5  8372  omeu  8576  expmordi  14235  hash7g  14555  4sqlem18  17060  vdwlem10  17088  0catg  17782  mvrf1  22206  mdetuni0  22849  mdetmul  22851  tsmsxp  24387  ax5seglem3  29396  btwnconn1lem1  36675  btwnconn1lem2  36676  btwnconn1lem3  36677  btwnconn1lem12  36686  btwnconn1lem13  36687  lshpkrlem6  39996  athgt  40337  2llnjN  40448  dalaw  40767  lhpmcvr4N  40907  cdlemb2  40922  4atexlemex6  40955  cdlemd7  41085  cdleme01N  41102  cdleme02N  41103  cdleme0ex1N  41104  cdleme0ex2N  41105  cdleme7aa  41123  cdleme7c  41126  cdleme7d  41127  cdleme7e  41128  cdleme7ga  41129  cdleme7  41130  cdleme11a  41141  cdleme20k  41200  cdleme27cl  41247  cdleme42e  41360  cdleme42h  41363  cdleme42i  41364  cdlemf  41444  cdlemg2kq  41483  cdlemg2m  41485  cdlemg8a  41508  cdlemg11aq  41519  cdlemg10c  41520  cdlemg11b  41523  cdlemg17a  41542  cdlemg31b0N  41575  cdlemg31c  41580  cdlemg33c0  41583  cdlemg41  41599  cdlemh2  41697  cdlemn9  42086  dihglbcpreN  42181  dihmeetlem3N  42186  dihmeetlem13N  42200  pellex  43684