Theorem simp2ll 1241

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  8420  omeu  8623  expmordi  14207  hash7g  14525  4sqlem18  17000  vdwlem10  17028  0catg  17731  mvrf1  22006  mdetuni0  22627  mdetmul  22629  tsmsxp  24163  ax5seglem3  28946  btwnconn1lem1  36088  btwnconn1lem2  36089  btwnconn1lem3  36090  btwnconn1lem12  36099  btwnconn1lem13  36100  lshpkrlem6  39116  athgt  39458  2llnjN  39569  dalaw  39888  lhpmcvr4N  40028  cdlemb2  40043  4atexlemex6  40076  cdlemd7  40206  cdleme01N  40223  cdleme02N  40224  cdleme0ex1N  40225  cdleme0ex2N  40226  cdleme7aa  40244  cdleme7c  40247  cdleme7d  40248  cdleme7e  40249  cdleme7ga  40250  cdleme7  40251  cdleme11a  40262  cdleme20k  40321  cdleme27cl  40368  cdleme42e  40481  cdleme42h  40484  cdleme42i  40485  cdlemf  40565  cdlemg2kq  40604  cdlemg2m  40606  cdlemg8a  40629  cdlemg11aq  40640  cdlemg10c  40641  cdlemg11b  40644  cdlemg17a  40663  cdlemg31b0N  40696  cdlemg31c  40701  cdlemg33c0  40704  cdlemg41  40720  cdlemh2  40818  cdlemn9  41207  dihglbcpreN  41302  dihmeetlem3N  41307  dihmeetlem13N  41321  pellex  42846