| 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 766 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑) | |
| 2 | 1 | 3ad2ant1 1133 | 1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
| 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 207 df-an 396 df-3an 1088 |
| This theorem is referenced by: lspsolvlem 21049 1marepvsma1 22468 mdetunilem8 22504 madutpos 22527 ax5seg 28883 rabfodom 32449 measinblem 34187 btwnconn1lem2 36062 btwnconn1lem13 36073 athgt 39435 llnle 39497 lplnle 39519 lhpexle1 39987 lhpj1 40001 lhpat3 40025 ltrncnv 40125 cdleme16aN 40238 tendoicl 40775 cdlemk55b 40939 dihatexv 41317 dihglblem6 41319 limccog 45601 icccncfext 45868 stoweidlem31 46012 stoweidlem34 46015 stoweidlem49 46030 stoweidlem57 46038 |
| Copyright terms: Public domain | W3C validator |