Theorem simp2ll 1242

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

Assertion

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

Proof of Theorem simp2ll

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

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

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 1089

This theorem is referenced by:  tfrlem5  8319  omeu  8520  expmordi  14129  hash7g  14448  4sqlem18  16933  vdwlem10  16961  0catg  17654  mvrf1  21964  mdetuni0  22586  mdetmul  22588  tsmsxp  24120  ax5seglem3  29000  btwnconn1lem1  36269  btwnconn1lem2  36270  btwnconn1lem3  36271  btwnconn1lem12  36280  btwnconn1lem13  36281  lshpkrlem6  39561  athgt  39902  2llnjN  40013  dalaw  40332  lhpmcvr4N  40472  cdlemb2  40487  4atexlemex6  40520  cdlemd7  40650  cdleme01N  40667  cdleme02N  40668  cdleme0ex1N  40669  cdleme0ex2N  40670  cdleme7aa  40688  cdleme7c  40691  cdleme7d  40692  cdleme7e  40693  cdleme7ga  40694  cdleme7  40695  cdleme11a  40706  cdleme20k  40765  cdleme27cl  40812  cdleme42e  40925  cdleme42h  40928  cdleme42i  40929  cdlemf  41009  cdlemg2kq  41048  cdlemg2m  41050  cdlemg8a  41073  cdlemg11aq  41084  cdlemg10c  41085  cdlemg11b  41088  cdlemg17a  41107  cdlemg31b0N  41140  cdlemg31c  41145  cdlemg33c0  41148  cdlemg41  41164  cdlemh2  41262  cdlemn9  41651  dihglbcpreN  41746  dihmeetlem3N  41751  dihmeetlem13N  41765  pellex  43263