Theorem simp1ll 1302

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

Assertion

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

Proof of Theorem simp1ll

Step	Hyp	Ref	Expression
1		simpll 750	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)
2	1	3ad2ant1 1127	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071

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 383  df-3an 1073

This theorem is referenced by:  lspsolvlem  19356  1marepvsma1  20607  mdetunilem8  20643  madutpos  20666  ax5seg  26039  rabfodom  29682  measinblem  30623  btwnconn1lem2  32532  btwnconn1lem13  32543  athgt  35264  llnle  35326  lplnle  35348  lhpexle1  35816  lhpj1  35830  lhpat3  35854  ltrncnv  35954  cdleme16aN  36068  tendoicl  36605  cdlemk55b  36769  dihatexv  37148  dihglblem6  37150  limccog  40370  icccncfext  40618  stoweidlem31  40765  stoweidlem34  40768  stoweidlem49  40783  stoweidlem57  40791