| 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 21097 1marepvsma1 22527 mdetunilem8 22563 madutpos 22586 bdayfinbndlem1 28463 ax5seg 29011 rabfodom 32580 measinblem 34377 btwnconn1lem2 36282 btwnconn1lem13 36293 athgt 39712 llnle 39774 lplnle 39796 lhpexle1 40264 lhpj1 40278 lhpat3 40302 ltrncnv 40402 cdleme16aN 40515 tendoicl 41052 cdlemk55b 41216 dihatexv 41594 dihglblem6 41596 limccog 45862 icccncfext 46127 stoweidlem31 46271 stoweidlem34 46274 stoweidlem49 46289 stoweidlem57 46297 |
| Copyright terms: Public domain | W3C validator |