Theorem simp2ll 1126

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp2ll	⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑)

Proof of Theorem simp2ll

Step	Hyp	Ref	Expression
1		simpll 789	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)
2	1	3ad2ant2 1081	1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036

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 197  df-an 386  df-3an 1038

This theorem is referenced by:  tfrlem5  7421  omeu  7610  4sqlem18  15590  vdwlem10  15618  0catg  16269  mvrf1  19344  mdetuni0  20346  mdetmul  20348  tsmsxp  21868  ax5seglem3  25711  btwnconn1lem1  31833  btwnconn1lem2  31834  btwnconn1lem3  31835  btwnconn1lem12  31844  btwnconn1lem13  31845  lshpkrlem6  33879  athgt  34219  2llnjN  34330  dalaw  34649  lhpmcvr4N  34789  cdlemb2  34804  4atexlemex6  34837  cdlemd7  34968  cdleme01N  34985  cdleme02N  34986  cdleme0ex1N  34987  cdleme0ex2N  34988  cdleme7aa  35006  cdleme7c  35009  cdleme7d  35010  cdleme7e  35011  cdleme7ga  35012  cdleme7  35013  cdleme11a  35024  cdleme20k  35084  cdleme27cl  35131  cdleme42e  35244  cdleme42h  35247  cdleme42i  35248  cdlemf  35328  cdlemg2kq  35367  cdlemg2m  35369  cdlemg8a  35392  cdlemg11aq  35403  cdlemg10c  35404  cdlemg11b  35407  cdlemg17a  35426  cdlemg31b0N  35459  cdlemg31c  35464  cdlemg33c0  35467  cdlemg41  35483  cdlemh2  35581  cdlemn9  35971  dihglbcpreN  36066  dihmeetlem3N  36071  dihmeetlem13N  36085  pellex  36876  expmordi  36989