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 766	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)
2	1	3ad2ant2 1134	1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  tfrlem5  8394  omeu  8597  expmordi  14185  hash7g  14504  4sqlem18  16982  vdwlem10  17010  0catg  17700  mvrf1  21946  mdetuni0  22559  mdetmul  22561  tsmsxp  24093  ax5seglem3  28910  btwnconn1lem1  36105  btwnconn1lem2  36106  btwnconn1lem3  36107  btwnconn1lem12  36116  btwnconn1lem13  36117  lshpkrlem6  39133  athgt  39475  2llnjN  39586  dalaw  39905  lhpmcvr4N  40045  cdlemb2  40060  4atexlemex6  40093  cdlemd7  40223  cdleme01N  40240  cdleme02N  40241  cdleme0ex1N  40242  cdleme0ex2N  40243  cdleme7aa  40261  cdleme7c  40264  cdleme7d  40265  cdleme7e  40266  cdleme7ga  40267  cdleme7  40268  cdleme11a  40279  cdleme20k  40338  cdleme27cl  40385  cdleme42e  40498  cdleme42h  40501  cdleme42i  40502  cdlemf  40582  cdlemg2kq  40621  cdlemg2m  40623  cdlemg8a  40646  cdlemg11aq  40657  cdlemg10c  40658  cdlemg11b  40661  cdlemg17a  40680  cdlemg31b0N  40713  cdlemg31c  40718  cdlemg33c0  40721  cdlemg41  40737  cdlemh2  40835  cdlemn9  41224  dihglbcpreN  41319  dihmeetlem3N  41324  dihmeetlem13N  41338  pellex  42858