I don't know if this will help, but I found proofs of mpi and a1d from
welsh's second axiom:
MM> show proof w2mpi
16 min=w2luk2 $p |- ( ( -. ps -> ps ) -> ps )
19 maj=w2ax1 $p |- ( ( ( -. ps -> ps ) -> ps ) -> ( -. ch -> ( ( -.
ps ->
ps ) -> ps )
) )
20 min=ax-mp $a |- ( -. ch -> ( ( -. ps -> ps ) -> ps ) )
29 min=w2mpi.2 $e |- ( ps -> ( ph -> ch ) )
34 min=w2mpi.1 $e |- ph
40 maj=ax-w2 $a |- ( ph -> ( ( ps -> ( ph -> ch ) ) -> ( ( -. ch ->
( (
-. ps -> ps ) -> ps ) ) -> ( ps -> ch ) )
) )
41 maj=ax-mp $a |- ( ( ps -> ( ph -> ch ) ) -> ( ( -. ch -> ( ( -. ps
->
ps ) -> ps ) ) -> ( ps -> ch )
) )
42 maj=ax-mp $a |- ( ( -. ch -> ( ( -. ps -> ps ) -> ps ) ) -> ( ps ->
ch )
)
43 w2mpi=ax-mp $a |- ( ps -> ch )
MM> show proof w2a1d
17 min=w2luk2 $p |- ( ( -. ch -> ch ) -> ch )
20 maj=w2ax1 $p |- ( ( ( -. ch -> ch ) -> ch ) -> ( -. ps -> ( ( -.
ch
-> ch ) -> ch )
) )
21 w2mpi.1=ax-mp $a |- ( -. ps -> ( ( -. ch -> ch ) -> ch ) )
33 min=w2a1d.1 $e |- ( ph -> ps )
36 maj=w2ax1 $p |- ( ( ph -> ps ) -> ( ch -> ( ph -> ps ) ) )
37 w2mpi.1=ax-mp $a |- ( ch -> ( ph -> ps ) )
43 w2mpi.2=ax-w2 $a |- ( ph -> ( ( ch -> ( ph -> ps ) ) -> ( ( -. ps ->
( (
-. ch -> ch ) -> ch ) ) -> ( ch -> ps ) )
) )
44 w2mpi.2=w2mpi $p |- ( ph -> ( ( -. ps -> ( ( -. ch -> ch ) -> ch ) )
-> (
ch -> ps )
) )
45 w2a1d=w2mpi $p |- ( ph -> ( ch -> ps ) )
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/2a5c8275-18a9-4c00-af2a-3f4d76be6768n%40googlegroups.com.
