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  8348  omeu  8549  expmordi  14132  hash7g  14451  4sqlem18  16933  vdwlem10  16961  0catg  17649  mvrf1  21895  mdetuni0  22508  mdetmul  22510  tsmsxp  24042  ax5seglem3  28858  btwnconn1lem1  36075  btwnconn1lem2  36076  btwnconn1lem3  36077  btwnconn1lem12  36086  btwnconn1lem13  36087  lshpkrlem6  39108  athgt  39450  2llnjN  39561  dalaw  39880  lhpmcvr4N  40020  cdlemb2  40035  4atexlemex6  40068  cdlemd7  40198  cdleme01N  40215  cdleme02N  40216  cdleme0ex1N  40217  cdleme0ex2N  40218  cdleme7aa  40236  cdleme7c  40239  cdleme7d  40240  cdleme7e  40241  cdleme7ga  40242  cdleme7  40243  cdleme11a  40254  cdleme20k  40313  cdleme27cl  40360  cdleme42e  40473  cdleme42h  40476  cdleme42i  40477  cdlemf  40557  cdlemg2kq  40596  cdlemg2m  40598  cdlemg8a  40621  cdlemg11aq  40632  cdlemg10c  40633  cdlemg11b  40636  cdlemg17a  40655  cdlemg31b0N  40688  cdlemg31c  40693  cdlemg33c0  40696  cdlemg41  40712  cdlemh2  40810  cdlemn9  41199  dihglbcpreN  41294  dihmeetlem3N  41299  dihmeetlem13N  41313  pellex  42823