Theorem simp1ll 1124

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

Assertion

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

Proof of Theorem simp1ll

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 386  df-3an 1039

This theorem is referenced by:  lspsolvlem  19142  1marepvsma1  20389  mdetunilem8  20425  madutpos  20448  ax5seg  25818  rabfodom  29344  measinblem  30283  btwnconn1lem2  32195  btwnconn1lem13  32206  athgt  34742  llnle  34804  lplnle  34826  lhpexle1  35294  lhpj1  35308  lhpat3  35332  ltrncnv  35432  cdleme16aN  35546  tendoicl  36084  cdlemk55b  36248  dihatexv  36627  dihglblem6  36629  limccog  39852  icccncfext  40100  stoweidlem31  40248  stoweidlem34  40251  stoweidlem49  40266  stoweidlem57  40274