Theorem simp2ll 1239

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 1133	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  8419  omeu  8622  expmordi  14204  hash7g  14522  4sqlem18  16996  vdwlem10  17024  0catg  17733  mvrf1  22024  mdetuni0  22643  mdetmul  22645  tsmsxp  24179  ax5seglem3  28961  btwnconn1lem1  36069  btwnconn1lem2  36070  btwnconn1lem3  36071  btwnconn1lem12  36080  btwnconn1lem13  36081  lshpkrlem6  39097  athgt  39439  2llnjN  39550  dalaw  39869  lhpmcvr4N  40009  cdlemb2  40024  4atexlemex6  40057  cdlemd7  40187  cdleme01N  40204  cdleme02N  40205  cdleme0ex1N  40206  cdleme0ex2N  40207  cdleme7aa  40225  cdleme7c  40228  cdleme7d  40229  cdleme7e  40230  cdleme7ga  40231  cdleme7  40232  cdleme11a  40243  cdleme20k  40302  cdleme27cl  40349  cdleme42e  40462  cdleme42h  40465  cdleme42i  40466  cdlemf  40546  cdlemg2kq  40585  cdlemg2m  40587  cdlemg8a  40610  cdlemg11aq  40621  cdlemg10c  40622  cdlemg11b  40625  cdlemg17a  40644  cdlemg31b0N  40677  cdlemg31c  40682  cdlemg33c0  40685  cdlemg41  40701  cdlemh2  40799  cdlemn9  41188  dihglbcpreN  41283  dihmeetlem3N  41288  dihmeetlem13N  41302  pellex  42823