Theorem simp3ll 1245

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

Assertion

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

Proof of Theorem simp3ll

Step	Hyp	Ref	Expression
1		simpll 767	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)
2	1	3ad2ant3 1136	1 ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1088

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 210  df-an 400  df-3an 1090

This theorem is referenced by:  f1oiso2  7131  omeu  8255  ntrivcvgmul  15363  tsmsxp  22919  tgqioo  23565  ovolunlem2  24263  plyadd  24979  plymul  24980  coeeu  24987  tghilberti2  26597  nosupbnd1lem2  33568  noinfbnd1lem2  33583  btwnconn1lem2  34046  btwnconn1lem3  34047  btwnconn1lem12  34056  athgt  37126  2llnjN  37237  4atlem12b  37281  lncmp  37453  cdlema2N  37462  cdlemc2  37862  cdleme5  37910  cdleme11a  37930  cdleme21ct  37999  cdleme21  38007  cdleme22eALTN  38015  cdleme24  38022  cdleme27cl  38036  cdleme27a  38037  cdleme28  38043  cdleme36a  38130  cdleme42b  38148  cdleme48fvg  38170  cdlemf  38233  cdlemk39  38586  cdlemkid1  38592  dihlsscpre  38904  dihord4  38928  dihord5apre  38932  dihmeetlem20N  38996  mapdh9a  39459  pellex  40270  jm2.27  40443