Theorem simp2ll 1238

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 1132	1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  tfrlem5  8394  omeu  8599  expmordi  14157  4sqlem18  16924  vdwlem10  16952  0catg  17661  mvrf1  21921  mdetuni0  22516  mdetmul  22518  tsmsxp  24052  ax5seglem3  28735  btwnconn1lem1  35673  btwnconn1lem2  35674  btwnconn1lem3  35675  btwnconn1lem12  35684  btwnconn1lem13  35685  lshpkrlem6  38576  athgt  38918  2llnjN  39029  dalaw  39348  lhpmcvr4N  39488  cdlemb2  39503  4atexlemex6  39536  cdlemd7  39666  cdleme01N  39683  cdleme02N  39684  cdleme0ex1N  39685  cdleme0ex2N  39686  cdleme7aa  39704  cdleme7c  39707  cdleme7d  39708  cdleme7e  39709  cdleme7ga  39710  cdleme7  39711  cdleme11a  39722  cdleme20k  39781  cdleme27cl  39828  cdleme42e  39941  cdleme42h  39944  cdleme42i  39945  cdlemf  40025  cdlemg2kq  40064  cdlemg2m  40066  cdlemg8a  40089  cdlemg11aq  40100  cdlemg10c  40101  cdlemg11b  40104  cdlemg17a  40123  cdlemg31b0N  40156  cdlemg31c  40161  cdlemg33c0  40164  cdlemg41  40180  cdlemh2  40278  cdlemn9  40667  dihglbcpreN  40762  dihmeetlem3N  40767  dihmeetlem13N  40781  pellex  42227