![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpisyl | Unicode version |
Description: A syllogism combined with a modus ponens inference. (Contributed by Alan Sare, 25-Jul-2011.) |
Ref | Expression |
---|---|
mpisyl.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
mpisyl.2 |
![]() ![]() |
mpisyl.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpisyl |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpisyl.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | mpisyl.2 |
. . 3
![]() ![]() | |
3 | mpisyl.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | mpi 15 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: ceqsex 2777 reusv1 4460 fliftcnv 5798 fliftfun 5799 tfrlemibfn 6331 tfr1onlembfn 6347 tfrcllembfn 6360 cnvct 6811 ordiso 7037 exmidomni 7142 djudoml 7220 djudomr 7221 uzsinds 10444 fimaxq 10809 ltoddhalfle 11900 phicl2 12216 strsetsid 12497 txdis1cn 13817 xmeter 13975 subctctexmid 14789 |
Copyright terms: Public domain | W3C validator |