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 62 | 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: relcnvtr 5028 relresfld 5038 relcoi1 5040 funco 5133 foimacnv 5353 fvi 5446 isoini2 5688 ovidig 5856 smores2 6159 tfrlem5 6179 snnen2og 6721 phpm 6727 fict 6730 infnfi 6757 isinfinf 6759 exmidpw 6770 difinfinf 6954 enumct 6968 exmidfodomrlemr 7026 exmidfodomrlemrALT 7027 isumz 11126 fsumsersdc 11132 isumclim 11158 isumclim3 11160 alzdvds 11479 zsupcl 11567 infssuzex 11569 gcddvds 11579 dvdslegcd 11580 ennnfonelemrn 11859 ctinf 11870 strle1g 11976 metrest 12602 dvef 12783 nnsf 13126 exmidsbthrlem 13144 |
Copyright terms: Public domain | W3C validator |