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  8305  omeu  8506  expmordi  14076  hash7g  14395  4sqlem18  16876  vdwlem10  16904  0catg  17596  mvrf1  21924  mdetuni0  22537  mdetmul  22539  tsmsxp  24071  ax5seglem3  28911  btwnconn1lem1  36152  btwnconn1lem2  36153  btwnconn1lem3  36154  btwnconn1lem12  36163  btwnconn1lem13  36164  lshpkrlem6  39235  athgt  39576  2llnjN  39687  dalaw  40006  lhpmcvr4N  40146  cdlemb2  40161  4atexlemex6  40194  cdlemd7  40324  cdleme01N  40341  cdleme02N  40342  cdleme0ex1N  40343  cdleme0ex2N  40344  cdleme7aa  40362  cdleme7c  40365  cdleme7d  40366  cdleme7e  40367  cdleme7ga  40368  cdleme7  40369  cdleme11a  40380  cdleme20k  40439  cdleme27cl  40486  cdleme42e  40599  cdleme42h  40602  cdleme42i  40603  cdlemf  40683  cdlemg2kq  40722  cdlemg2m  40724  cdlemg8a  40747  cdlemg11aq  40758  cdlemg10c  40759  cdlemg11b  40762  cdlemg17a  40781  cdlemg31b0N  40814  cdlemg31c  40819  cdlemg33c0  40822  cdlemg41  40838  cdlemh2  40936  cdlemn9  41325  dihglbcpreN  41420  dihmeetlem3N  41425  dihmeetlem13N  41439  pellex  42953