Theorem simp2ll 1257

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

Assertion

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

Proof of Theorem simp2ll

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  tfrlem5  8354  omeu  8558  expmordi  14191  hash7g  14511  4sqlem18  17010  vdwlem10  17038  0catg  17732  mvrf1  22092  mdetuni0  22735  mdetmul  22737  tsmsxp  24269  ax5seglem3  29186  btwnconn1lem1  36445  btwnconn1lem2  36446  btwnconn1lem3  36447  btwnconn1lem12  36456  btwnconn1lem13  36457  lshpkrlem6  39746  athgt  40087  2llnjN  40198  dalaw  40517  lhpmcvr4N  40657  cdlemb2  40672  4atexlemex6  40705  cdlemd7  40835  cdleme01N  40852  cdleme02N  40853  cdleme0ex1N  40854  cdleme0ex2N  40855  cdleme7aa  40873  cdleme7c  40876  cdleme7d  40877  cdleme7e  40878  cdleme7ga  40879  cdleme7  40880  cdleme11a  40891  cdleme20k  40950  cdleme27cl  40997  cdleme42e  41110  cdleme42h  41113  cdleme42i  41114  cdlemf  41194  cdlemg2kq  41233  cdlemg2m  41235  cdlemg8a  41258  cdlemg11aq  41269  cdlemg10c  41270  cdlemg11b  41273  cdlemg17a  41292  cdlemg31b0N  41325  cdlemg31c  41330  cdlemg33c0  41333  cdlemg41  41349  cdlemh2  41447  cdlemn9  41836  dihglbcpreN  41931  dihmeetlem3N  41936  dihmeetlem13N  41950  pellex  43419