Theorem simp2ll 1259

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

Assertion

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

Proof of Theorem simp2ll

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  tfrlem5  8390  omeu  8596  expmordi  14313  hash7g  14634  4sqlem18  17145  vdwlem10  17173  0catg  17867  mvrf1  22298  mdetuni0  22941  mdetmul  22943  tsmsxp  24479  ax5seglem3  29514  btwnconn1lem1  36944  btwnconn1lem2  36945  btwnconn1lem3  36946  btwnconn1lem12  36955  btwnconn1lem13  36956  lshpkrlem6  40265  athgt  40606  2llnjN  40717  dalaw  41036  lhpmcvr4N  41176  cdlemb2  41191  4atexlemex6  41224  cdlemd7  41354  cdleme01N  41371  cdleme02N  41372  cdleme0ex1N  41373  cdleme0ex2N  41374  cdleme7aa  41392  cdleme7c  41395  cdleme7d  41396  cdleme7e  41397  cdleme7ga  41398  cdleme7  41399  cdleme11a  41410  cdleme20k  41469  cdleme27cl  41516  cdleme42e  41629  cdleme42h  41632  cdleme42i  41633  cdlemf  41713  cdlemg2kq  41752  cdlemg2m  41754  cdlemg8a  41777  cdlemg11aq  41788  cdlemg10c  41789  cdlemg11b  41792  cdlemg17a  41811  cdlemg31b0N  41844  cdlemg31c  41849  cdlemg33c0  41852  cdlemg41  41868  cdlemh2  41966  cdlemn9  42355  dihglbcpreN  42450  dihmeetlem3N  42455  dihmeetlem13N  42469  pellex  43935