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  8321  omeu  8522  expmordi  14102  hash7g  14421  4sqlem18  16902  vdwlem10  16930  0catg  17623  mvrf1  21953  mdetuni0  22577  mdetmul  22579  tsmsxp  24111  ax5seglem3  29016  btwnconn1lem1  36300  btwnconn1lem2  36301  btwnconn1lem3  36302  btwnconn1lem12  36311  btwnconn1lem13  36312  lshpkrlem6  39485  athgt  39826  2llnjN  39937  dalaw  40256  lhpmcvr4N  40396  cdlemb2  40411  4atexlemex6  40444  cdlemd7  40574  cdleme01N  40591  cdleme02N  40592  cdleme0ex1N  40593  cdleme0ex2N  40594  cdleme7aa  40612  cdleme7c  40615  cdleme7d  40616  cdleme7e  40617  cdleme7ga  40618  cdleme7  40619  cdleme11a  40630  cdleme20k  40689  cdleme27cl  40736  cdleme42e  40849  cdleme42h  40852  cdleme42i  40853  cdlemf  40933  cdlemg2kq  40972  cdlemg2m  40974  cdlemg8a  40997  cdlemg11aq  41008  cdlemg10c  41009  cdlemg11b  41012  cdlemg17a  41031  cdlemg31b0N  41064  cdlemg31c  41069  cdlemg33c0  41072  cdlemg41  41088  cdlemh2  41186  cdlemn9  41575  dihglbcpreN  41670  dihmeetlem3N  41675  dihmeetlem13N  41689  pellex  43186