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 766	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)
2	1	3ad2ant2 1134	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  8436  omeu  8641  expmordi  14217  hash7g  14535  4sqlem18  17009  vdwlem10  17037  0catg  17746  mvrf1  22029  mdetuni0  22648  mdetmul  22650  tsmsxp  24184  ax5seglem3  28964  btwnconn1lem1  36051  btwnconn1lem2  36052  btwnconn1lem3  36053  btwnconn1lem12  36062  btwnconn1lem13  36063  lshpkrlem6  39071  athgt  39413  2llnjN  39524  dalaw  39843  lhpmcvr4N  39983  cdlemb2  39998  4atexlemex6  40031  cdlemd7  40161  cdleme01N  40178  cdleme02N  40179  cdleme0ex1N  40180  cdleme0ex2N  40181  cdleme7aa  40199  cdleme7c  40202  cdleme7d  40203  cdleme7e  40204  cdleme7ga  40205  cdleme7  40206  cdleme11a  40217  cdleme20k  40276  cdleme27cl  40323  cdleme42e  40436  cdleme42h  40439  cdleme42i  40440  cdlemf  40520  cdlemg2kq  40559  cdlemg2m  40561  cdlemg8a  40584  cdlemg11aq  40595  cdlemg10c  40596  cdlemg11b  40599  cdlemg17a  40618  cdlemg31b0N  40651  cdlemg31c  40656  cdlemg33c0  40659  cdlemg41  40675  cdlemh2  40773  cdlemn9  41162  dihglbcpreN  41257  dihmeetlem3N  41262  dihmeetlem13N  41276  pellex  42791