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  8182  omeu  8378  expmordi  13813  4sqlem18  16591  vdwlem10  16619  0catg  17314  mvrf1  21104  mdetuni0  21678  mdetmul  21680  tsmsxp  23214  ax5seglem3  27202  btwnconn1lem1  34316  btwnconn1lem2  34317  btwnconn1lem3  34318  btwnconn1lem12  34327  btwnconn1lem13  34328  lshpkrlem6  37056  athgt  37397  2llnjN  37508  dalaw  37827  lhpmcvr4N  37967  cdlemb2  37982  4atexlemex6  38015  cdlemd7  38145  cdleme01N  38162  cdleme02N  38163  cdleme0ex1N  38164  cdleme0ex2N  38165  cdleme7aa  38183  cdleme7c  38186  cdleme7d  38187  cdleme7e  38188  cdleme7ga  38189  cdleme7  38190  cdleme11a  38201  cdleme20k  38260  cdleme27cl  38307  cdleme42e  38420  cdleme42h  38423  cdleme42i  38424  cdlemf  38504  cdlemg2kq  38543  cdlemg2m  38545  cdlemg8a  38568  cdlemg11aq  38579  cdlemg10c  38580  cdlemg11b  38583  cdlemg17a  38602  cdlemg31b0N  38635  cdlemg31c  38640  cdlemg33c0  38643  cdlemg41  38659  cdlemh2  38757  cdlemn9  39146  dihglbcpreN  39241  dihmeetlem3N  39246  dihmeetlem13N  39260  pellex  40573