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  8371  omeu  8577  expmordi  14290  hash7g  14611  4sqlem18  17120  vdwlem10  17148  0catg  17842  mvrf1  22273  mdetuni0  22916  mdetmul  22918  tsmsxp  24454  ax5seglem3  29491  btwnconn1lem1  36822  btwnconn1lem2  36823  btwnconn1lem3  36824  btwnconn1lem12  36833  btwnconn1lem13  36834  lshpkrlem6  40140  athgt  40481  2llnjN  40592  dalaw  40911  lhpmcvr4N  41051  cdlemb2  41066  4atexlemex6  41099  cdlemd7  41229  cdleme01N  41246  cdleme02N  41247  cdleme0ex1N  41248  cdleme0ex2N  41249  cdleme7aa  41267  cdleme7c  41270  cdleme7d  41271  cdleme7e  41272  cdleme7ga  41273  cdleme7  41274  cdleme11a  41285  cdleme20k  41344  cdleme27cl  41391  cdleme42e  41504  cdleme42h  41507  cdleme42i  41508  cdlemf  41588  cdlemg2kq  41627  cdlemg2m  41629  cdlemg8a  41652  cdlemg11aq  41663  cdlemg10c  41664  cdlemg11b  41667  cdlemg17a  41686  cdlemg31b0N  41719  cdlemg31c  41724  cdlemg33c0  41727  cdlemg41  41743  cdlemh2  41841  cdlemn9  42230  dihglbcpreN  42325  dihmeetlem3N  42330  dihmeetlem13N  42344  pellex  43795