![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpsyl | Unicode version |
Description: Modus ponens combined with a syllogism inference. (Contributed by Alan Sare, 20-Apr-2011.) |
Ref | Expression |
---|---|
mpsyl.1 |
![]() ![]() |
mpsyl.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
mpsyl.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpsyl |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpsyl.1 |
. . 3
![]() ![]() | |
2 | 1 | a1i 9 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
3 | mpsyl.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | mpsyl.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | sylc 56 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: relcnvtr 4840 relresfld 4847 relcoi1 4849 funco 4940 foimacnv 5144 fvi 5230 isoini2 5458 ovidig 5618 smores2 5909 tfrlem5 5930 snnen2og 6322 phpm 6327 cauappcvgprlemm 6743 caucvgprlemm 6766 caucvgprprlemml 6792 caucvgsr 6886 |
Copyright terms: Public domain | W3C validator |