Theorem simp2ll 1240

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

Assertion

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

Proof of Theorem simp2ll

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  tfrlem5  8379  omeu  8584  expmordi  14131  4sqlem18  16894  vdwlem10  16922  0catg  17631  mvrf1  21544  mdetuni0  22122  mdetmul  22124  tsmsxp  23658  ax5seglem3  28186  btwnconn1lem1  35054  btwnconn1lem2  35055  btwnconn1lem3  35056  btwnconn1lem12  35065  btwnconn1lem13  35066  lshpkrlem6  37980  athgt  38322  2llnjN  38433  dalaw  38752  lhpmcvr4N  38892  cdlemb2  38907  4atexlemex6  38940  cdlemd7  39070  cdleme01N  39087  cdleme02N  39088  cdleme0ex1N  39089  cdleme0ex2N  39090  cdleme7aa  39108  cdleme7c  39111  cdleme7d  39112  cdleme7e  39113  cdleme7ga  39114  cdleme7  39115  cdleme11a  39126  cdleme20k  39185  cdleme27cl  39232  cdleme42e  39345  cdleme42h  39348  cdleme42i  39349  cdlemf  39429  cdlemg2kq  39468  cdlemg2m  39470  cdlemg8a  39493  cdlemg11aq  39504  cdlemg10c  39505  cdlemg11b  39508  cdlemg17a  39527  cdlemg31b0N  39560  cdlemg31c  39565  cdlemg33c0  39568  cdlemg41  39584  cdlemh2  39682  cdlemn9  40071  dihglbcpreN  40166  dihmeetlem3N  40171  dihmeetlem13N  40185  pellex  41563