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: wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: ceqsex 2719 reusv1 4374 fliftcnv 5689 fliftfun 5690 tfrlemibfn 6218 tfr1onlembfn 6234 tfrcllembfn 6247 cnvct 6696 ordiso 6914 exmidomni 7007 djudoml 7068 djudomr 7069 uzsinds 10208 fimaxq 10566 ltoddhalfle 11579 phicl2 11879 strsetsid 11981 txdis1cn 12436 xmeter 12594 subctctexmid 13185 |
Copyright terms: Public domain | W3C validator |