![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp1ll | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp1ll | ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpll 765 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑) | |
2 | 1 | 3ad2ant1 1130 | 1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 206 df-an 395 df-3an 1086 |
This theorem is referenced by: lspsolvlem 21035 1marepvsma1 22503 mdetunilem8 22539 madutpos 22562 ax5seg 28767 rabfodom 32319 measinblem 33844 btwnconn1lem2 35689 btwnconn1lem13 35700 athgt 38933 llnle 38995 lplnle 39017 lhpexle1 39485 lhpj1 39499 lhpat3 39523 ltrncnv 39623 cdleme16aN 39736 tendoicl 40273 cdlemk55b 40437 dihatexv 40815 dihglblem6 40817 limccog 45010 icccncfext 45277 stoweidlem31 45421 stoweidlem34 45424 stoweidlem49 45439 stoweidlem57 45447 |
Copyright terms: Public domain | W3C validator |