Theorem simp2ll 1247

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

Assertion

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

Proof of Theorem simp2ll

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  tfrlem5  8316  omeu  8517  expmordi  14127  hash7g  14446  4sqlem18  16931  vdwlem10  16959  0catg  17652  mvrf1  21967  mdetuni0  22611  mdetmul  22613  tsmsxp  24145  ax5seglem3  29025  btwnconn1lem1  36322  btwnconn1lem2  36323  btwnconn1lem3  36324  btwnconn1lem12  36333  btwnconn1lem13  36334  lshpkrlem6  39614  athgt  39955  2llnjN  40066  dalaw  40385  lhpmcvr4N  40525  cdlemb2  40540  4atexlemex6  40573  cdlemd7  40703  cdleme01N  40720  cdleme02N  40721  cdleme0ex1N  40722  cdleme0ex2N  40723  cdleme7aa  40741  cdleme7c  40744  cdleme7d  40745  cdleme7e  40746  cdleme7ga  40747  cdleme7  40748  cdleme11a  40759  cdleme20k  40818  cdleme27cl  40865  cdleme42e  40978  cdleme42h  40981  cdleme42i  40982  cdlemf  41062  cdlemg2kq  41101  cdlemg2m  41103  cdlemg8a  41126  cdlemg11aq  41137  cdlemg10c  41138  cdlemg11b  41141  cdlemg17a  41160  cdlemg31b0N  41193  cdlemg31c  41198  cdlemg33c0  41201  cdlemg41  41217  cdlemh2  41315  cdlemn9  41704  dihglbcpreN  41799  dihmeetlem3N  41804  dihmeetlem13N  41818  pellex  43287