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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  tfrlem5  8380  omeu  8585  expmordi  14132  4sqlem18  16895  vdwlem10  16923  0catg  17632  mvrf1  21545  mdetuni0  22123  mdetmul  22125  tsmsxp  23659  ax5seglem3  28189  btwnconn1lem1  35059  btwnconn1lem2  35060  btwnconn1lem3  35061  btwnconn1lem12  35070  btwnconn1lem13  35071  lshpkrlem6  37985  athgt  38327  2llnjN  38438  dalaw  38757  lhpmcvr4N  38897  cdlemb2  38912  4atexlemex6  38945  cdlemd7  39075  cdleme01N  39092  cdleme02N  39093  cdleme0ex1N  39094  cdleme0ex2N  39095  cdleme7aa  39113  cdleme7c  39116  cdleme7d  39117  cdleme7e  39118  cdleme7ga  39119  cdleme7  39120  cdleme11a  39131  cdleme20k  39190  cdleme27cl  39237  cdleme42e  39350  cdleme42h  39353  cdleme42i  39354  cdlemf  39434  cdlemg2kq  39473  cdlemg2m  39475  cdlemg8a  39498  cdlemg11aq  39509  cdlemg10c  39510  cdlemg11b  39513  cdlemg17a  39532  cdlemg31b0N  39565  cdlemg31c  39570  cdlemg33c0  39573  cdlemg41  39589  cdlemh2  39687  cdlemn9  40076  dihglbcpreN  40171  dihmeetlem3N  40176  dihmeetlem13N  40190  pellex  41573