Theorem simp2ll 1241

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

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

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  tfrlem5  8309  omeu  8510  expmordi  14092  hash7g  14411  4sqlem18  16892  vdwlem10  16920  0catg  17612  mvrf1  21911  mdetuni0  22524  mdetmul  22526  tsmsxp  24058  ax5seglem3  28894  btwnconn1lem1  36060  btwnconn1lem2  36061  btwnconn1lem3  36062  btwnconn1lem12  36071  btwnconn1lem13  36072  lshpkrlem6  39093  athgt  39435  2llnjN  39546  dalaw  39865  lhpmcvr4N  40005  cdlemb2  40020  4atexlemex6  40053  cdlemd7  40183  cdleme01N  40200  cdleme02N  40201  cdleme0ex1N  40202  cdleme0ex2N  40203  cdleme7aa  40221  cdleme7c  40224  cdleme7d  40225  cdleme7e  40226  cdleme7ga  40227  cdleme7  40228  cdleme11a  40239  cdleme20k  40298  cdleme27cl  40345  cdleme42e  40458  cdleme42h  40461  cdleme42i  40462  cdlemf  40542  cdlemg2kq  40581  cdlemg2m  40583  cdlemg8a  40606  cdlemg11aq  40617  cdlemg10c  40618  cdlemg11b  40621  cdlemg17a  40640  cdlemg31b0N  40673  cdlemg31c  40678  cdlemg33c0  40681  cdlemg41  40697  cdlemh2  40795  cdlemn9  41184  dihglbcpreN  41279  dihmeetlem3N  41284  dihmeetlem13N  41298  pellex  42808