Theorem simp1ll 1232

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

Assertion

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

Proof of Theorem simp1ll

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  lspsolvlem  19914  1marepvsma1  21192  mdetunilem8  21228  madutpos  21251  ax5seg  26724  rabfodom  30266  measinblem  31479  btwnconn1lem2  33549  btwnconn1lem13  33560  athgt  36607  llnle  36669  lplnle  36691  lhpexle1  37159  lhpj1  37173  lhpat3  37197  ltrncnv  37297  cdleme16aN  37410  tendoicl  37947  cdlemk55b  38111  dihatexv  38489  dihglblem6  38491  limccog  41921  icccncfext  42190  stoweidlem31  42336  stoweidlem34  42339  stoweidlem49  42354  stoweidlem57  42362