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  8350  omeu  8551  expmordi  14138  hash7g  14457  4sqlem18  16939  vdwlem10  16967  0catg  17655  mvrf1  21901  mdetuni0  22514  mdetmul  22516  tsmsxp  24048  ax5seglem3  28864  btwnconn1lem1  36070  btwnconn1lem2  36071  btwnconn1lem3  36072  btwnconn1lem12  36081  btwnconn1lem13  36082  lshpkrlem6  39103  athgt  39445  2llnjN  39556  dalaw  39875  lhpmcvr4N  40015  cdlemb2  40030  4atexlemex6  40063  cdlemd7  40193  cdleme01N  40210  cdleme02N  40211  cdleme0ex1N  40212  cdleme0ex2N  40213  cdleme7aa  40231  cdleme7c  40234  cdleme7d  40235  cdleme7e  40236  cdleme7ga  40237  cdleme7  40238  cdleme11a  40249  cdleme20k  40308  cdleme27cl  40355  cdleme42e  40468  cdleme42h  40471  cdleme42i  40472  cdlemf  40552  cdlemg2kq  40591  cdlemg2m  40593  cdlemg8a  40616  cdlemg11aq  40627  cdlemg10c  40628  cdlemg11b  40631  cdlemg17a  40650  cdlemg31b0N  40683  cdlemg31c  40688  cdlemg33c0  40691  cdlemg41  40707  cdlemh2  40805  cdlemn9  41194  dihglbcpreN  41289  dihmeetlem3N  41294  dihmeetlem13N  41308  pellex  42816