Theorem simp2ll 1121

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

Assertion

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

Proof of Theorem simp2ll

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  tfrlem5  7363  omeu  7552  4sqlem18  15504  vdwlem10  15532  0catg  16171  mvrf1  19246  mdetuni0  20246  mdetmul  20248  tsmsxp  21768  ax5seglem3  25611  btwnconn1lem1  31364  btwnconn1lem2  31365  btwnconn1lem3  31366  btwnconn1lem12  31375  btwnconn1lem13  31376  lshpkrlem6  33420  athgt  33760  2llnjN  33871  dalaw  34190  lhpmcvr4N  34330  cdlemb2  34345  4atexlemex6  34378  cdlemd7  34509  cdleme01N  34526  cdleme02N  34527  cdleme0ex1N  34528  cdleme0ex2N  34529  cdleme7aa  34547  cdleme7c  34550  cdleme7d  34551  cdleme7e  34552  cdleme7ga  34553  cdleme7  34554  cdleme11a  34565  cdleme20k  34625  cdleme27cl  34672  cdleme42e  34785  cdleme42h  34788  cdleme42i  34789  cdlemf  34869  cdlemg2kq  34908  cdlemg2m  34910  cdlemg8a  34933  cdlemg11aq  34944  cdlemg10c  34945  cdlemg11b  34948  cdlemg17a  34967  cdlemg31b0N  35000  cdlemg31c  35005  cdlemg33c0  35008  cdlemg41  35024  cdlemh2  35122  cdlemn9  35512  dihglbcpreN  35607  dihmeetlem3N  35612  dihmeetlem13N  35626  pellex  36417  expmordi  36530