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 763	. 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  8195  omeu  8392  expmordi  13866  4sqlem18  16644  vdwlem10  16672  0catg  17378  mvrf1  21175  mdetuni0  21751  mdetmul  21753  tsmsxp  23287  ax5seglem3  27280  btwnconn1lem1  34368  btwnconn1lem2  34369  btwnconn1lem3  34370  btwnconn1lem12  34379  btwnconn1lem13  34380  lshpkrlem6  37108  athgt  37449  2llnjN  37560  dalaw  37879  lhpmcvr4N  38019  cdlemb2  38034  4atexlemex6  38067  cdlemd7  38197  cdleme01N  38214  cdleme02N  38215  cdleme0ex1N  38216  cdleme0ex2N  38217  cdleme7aa  38235  cdleme7c  38238  cdleme7d  38239  cdleme7e  38240  cdleme7ga  38241  cdleme7  38242  cdleme11a  38253  cdleme20k  38312  cdleme27cl  38359  cdleme42e  38472  cdleme42h  38475  cdleme42i  38476  cdlemf  38556  cdlemg2kq  38595  cdlemg2m  38597  cdlemg8a  38620  cdlemg11aq  38631  cdlemg10c  38632  cdlemg11b  38635  cdlemg17a  38654  cdlemg31b0N  38687  cdlemg31c  38692  cdlemg33c0  38695  cdlemg41  38711  cdlemh2  38809  cdlemn9  39198  dihglbcpreN  39293  dihmeetlem3N  39298  dihmeetlem13N  39312  pellex  40637