Theorem simp2ll 1242

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

Assertion

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

Proof of Theorem simp2ll

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

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

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 1089

This theorem is referenced by:  tfrlem5  8312  omeu  8513  expmordi  14120  hash7g  14439  4sqlem18  16924  vdwlem10  16952  0catg  17645  mvrf1  21974  mdetuni0  22596  mdetmul  22598  tsmsxp  24130  ax5seglem3  29014  btwnconn1lem1  36285  btwnconn1lem2  36286  btwnconn1lem3  36287  btwnconn1lem12  36296  btwnconn1lem13  36297  lshpkrlem6  39575  athgt  39916  2llnjN  40027  dalaw  40346  lhpmcvr4N  40486  cdlemb2  40501  4atexlemex6  40534  cdlemd7  40664  cdleme01N  40681  cdleme02N  40682  cdleme0ex1N  40683  cdleme0ex2N  40684  cdleme7aa  40702  cdleme7c  40705  cdleme7d  40706  cdleme7e  40707  cdleme7ga  40708  cdleme7  40709  cdleme11a  40720  cdleme20k  40779  cdleme27cl  40826  cdleme42e  40939  cdleme42h  40942  cdleme42i  40943  cdlemf  41023  cdlemg2kq  41062  cdlemg2m  41064  cdlemg8a  41087  cdlemg11aq  41098  cdlemg10c  41099  cdlemg11b  41102  cdlemg17a  41121  cdlemg31b0N  41154  cdlemg31c  41159  cdlemg33c0  41162  cdlemg41  41178  cdlemh2  41276  cdlemn9  41665  dihglbcpreN  41760  dihmeetlem3N  41765  dihmeetlem13N  41779  pellex  43281