Theorem simp2ll 1307

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

Assertion

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

Proof of Theorem simp2ll

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

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

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  tfrlem5  7641  omeu  7830  4sqlem18  15864  vdwlem10  15892  0catg  16545  mvrf1  19623  mdetuni0  20625  mdetmul  20627  tsmsxp  22155  ax5seglem3  26006  btwnconn1lem1  32496  btwnconn1lem2  32497  btwnconn1lem3  32498  btwnconn1lem12  32507  btwnconn1lem13  32508  lshpkrlem6  34901  athgt  35241  2llnjN  35352  dalaw  35671  lhpmcvr4N  35811  cdlemb2  35826  4atexlemex6  35859  cdlemd7  35990  cdleme01N  36007  cdleme02N  36008  cdleme0ex1N  36009  cdleme0ex2N  36010  cdleme7aa  36028  cdleme7c  36031  cdleme7d  36032  cdleme7e  36033  cdleme7ga  36034  cdleme7  36035  cdleme11a  36046  cdleme20k  36105  cdleme27cl  36152  cdleme42e  36265  cdleme42h  36268  cdleme42i  36269  cdlemf  36349  cdlemg2kq  36388  cdlemg2m  36390  cdlemg8a  36413  cdlemg11aq  36424  cdlemg10c  36425  cdlemg11b  36428  cdlemg17a  36447  cdlemg31b0N  36480  cdlemg31c  36485  cdlemg33c0  36488  cdlemg41  36504  cdlemh2  36602  cdlemn9  36992  dihglbcpreN  37087  dihmeetlem3N  37092  dihmeetlem13N  37106  pellex  37897  expmordi  38010