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  8299  omeu  8500  expmordi  14074  hash7g  14393  4sqlem18  16874  vdwlem10  16902  0catg  17594  mvrf1  21924  mdetuni0  22537  mdetmul  22539  tsmsxp  24071  ax5seglem3  28910  btwnconn1lem1  36127  btwnconn1lem2  36128  btwnconn1lem3  36129  btwnconn1lem12  36138  btwnconn1lem13  36139  lshpkrlem6  39160  athgt  39501  2llnjN  39612  dalaw  39931  lhpmcvr4N  40071  cdlemb2  40086  4atexlemex6  40119  cdlemd7  40249  cdleme01N  40266  cdleme02N  40267  cdleme0ex1N  40268  cdleme0ex2N  40269  cdleme7aa  40287  cdleme7c  40290  cdleme7d  40291  cdleme7e  40292  cdleme7ga  40293  cdleme7  40294  cdleme11a  40305  cdleme20k  40364  cdleme27cl  40411  cdleme42e  40524  cdleme42h  40527  cdleme42i  40528  cdlemf  40608  cdlemg2kq  40647  cdlemg2m  40649  cdlemg8a  40672  cdlemg11aq  40683  cdlemg10c  40684  cdlemg11b  40687  cdlemg17a  40706  cdlemg31b0N  40739  cdlemg31c  40744  cdlemg33c0  40747  cdlemg41  40763  cdlemh2  40861  cdlemn9  41250  dihglbcpreN  41345  dihmeetlem3N  41350  dihmeetlem13N  41364  pellex  42874