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 786 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑) | |
2 | 1 | 3ad2ant1 1075 | 1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: lspsolvlem 18963 1marepvsma1 20208 mdetunilem8 20244 madutpos 20267 ax5seg 25618 rabfodom 28728 measinblem 29610 btwnconn1lem2 31365 btwnconn1lem13 31376 athgt 33760 llnle 33822 lplnle 33844 lhpexle1 34312 lhpj1 34326 lhpat3 34350 ltrncnv 34450 cdleme16aN 34564 tendoicl 35102 cdlemk55b 35266 dihatexv 35645 dihglblem6 35647 limccog 38687 icccncfext 38773 stoweidlem31 38924 stoweidlem34 38927 stoweidlem49 38942 stoweidlem57 38950 |
Copyright terms: Public domain | W3C validator |