Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > wlkdlem4 | Structured version Visualization version Unicode version | ||
| Description: Lemma 4 for wlkd 26583. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 23-Jan-2021.) |
| Ref | Expression |
|---|---|
| wlkd.p |
      Word   |
| wlkd.f |
 Word |
| wlkd.l |
     |
| wlkd.e |
   ..^     |
| wlkd.n |
..^  |
| Ref | Expression |
|---|---|
| wlkdlem4 |
..^if- |
, , , ,| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wlkd.e |
. 2
..^ | |
| 2 | wlkd.n |
. 2
..^ | |
| 3 | r19.26 3064 |
. . 3
..^ ![/\](wedge.gif "/\"){kind=small} 
..^
..^ | |
| 4 | df-ne 2795 |
. . . . . 6
 | |
| 5 | ifpfal 1024 |
. . . . . 6
if-
| |
| 6 | 4, 5 | sylbi 207 |
. . . . 5
if-
|
| 7 | 6 | biimparc 504 |
. . . 4
if- |
| 8 | 7 | ralimi 2952 |
. . 3
..^ ..^if- |
| 9 | 3, 8 | sylbir 225 |
. 2
..^
..^
..^if- |
| 10 | 1, 2, 9 | syl2anc 693 |
1
..^if- |
| Colors of variables: wff setvar class |
| Syntax hints: wn 3
wi 4
wb 196 wa 384 if-wif 1012 wceq 1483 wcel 1990 wne 2794 wral 2912 cvv 3200 wss 3574 csn 4177 cpr 4179 cfv 5888 (class class class)co 6650
cc0 9936
c1 9937
caddc 9939 ..^cfzo 12465
chash 13117 Word cword 13291 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 |
| This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-ifp 1013 df-ne 2795 df-ral 2917 |
| This theorem is referenced by: wlkd 26583 |
| Copyright terms: Public domain | W3C validator |