Theorem simp2ll 1237

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  tfrlem5  7999  omeu  8194  expmordi  13527  4sqlem18  16288  vdwlem10  16316  0catg  16950  mvrf1  20663  mdetuni0  21226  mdetmul  21228  tsmsxp  22760  ax5seglem3  26725  btwnconn1lem1  33661  btwnconn1lem2  33662  btwnconn1lem3  33663  btwnconn1lem12  33672  btwnconn1lem13  33673  lshpkrlem6  36411  athgt  36752  2llnjN  36863  dalaw  37182  lhpmcvr4N  37322  cdlemb2  37337  4atexlemex6  37370  cdlemd7  37500  cdleme01N  37517  cdleme02N  37518  cdleme0ex1N  37519  cdleme0ex2N  37520  cdleme7aa  37538  cdleme7c  37541  cdleme7d  37542  cdleme7e  37543  cdleme7ga  37544  cdleme7  37545  cdleme11a  37556  cdleme20k  37615  cdleme27cl  37662  cdleme42e  37775  cdleme42h  37778  cdleme42i  37779  cdlemf  37859  cdlemg2kq  37898  cdlemg2m  37900  cdlemg8a  37923  cdlemg11aq  37934  cdlemg10c  37935  cdlemg11b  37938  cdlemg17a  37957  cdlemg31b0N  37990  cdlemg31c  37995  cdlemg33c0  37998  cdlemg41  38014  cdlemh2  38112  cdlemn9  38501  dihglbcpreN  38596  dihmeetlem3N  38601  dihmeetlem13N  38615  pellex  39776