![]() |
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: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: snssg 3728 relcnvtr 5150 relresfld 5160 relcoi1 5162 funco 5258 foimacnv 5481 fvi 5575 isoini2 5822 ovidig 5994 smores2 6297 tfrlem5 6317 snnen2og 6861 phpm 6867 fict 6870 infnfi 6897 isinfinf 6899 exmidpw 6910 difinfinf 7102 enumct 7116 exmidfodomrlemr 7203 exmidfodomrlemrALT 7204 isumz 11399 fsumsersdc 11405 isumclim 11431 isumclim3 11433 zprodap0 11591 alzdvds 11862 zsupcl 11950 infssuzex 11952 gcddvds 11966 dvdslegcd 11967 pclemub 12289 ennnfonelemj0 12404 ennnfonelemg 12406 ennnfonelemrn 12422 ctinf 12433 strle1g 12567 fnpr2ob 12764 metrest 14045 dvef 14227 bj-charfunbi 14602 pw1nct 14791 nnsf 14793 exmidsbthrlem 14809 |
Copyright terms: Public domain | W3C validator |