![]() |
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 3726 relcnvtr 5148 relresfld 5158 relcoi1 5160 funco 5256 foimacnv 5479 fvi 5573 isoini2 5819 ovidig 5991 smores2 6294 tfrlem5 6314 snnen2og 6858 phpm 6864 fict 6867 infnfi 6894 isinfinf 6896 exmidpw 6907 difinfinf 7099 enumct 7113 exmidfodomrlemr 7200 exmidfodomrlemrALT 7201 isumz 11396 fsumsersdc 11402 isumclim 11428 isumclim3 11430 zprodap0 11588 alzdvds 11859 zsupcl 11947 infssuzex 11949 gcddvds 11963 dvdslegcd 11964 pclemub 12286 ennnfonelemj0 12401 ennnfonelemg 12403 ennnfonelemrn 12419 ctinf 12430 strle1g 12564 fnpr2ob 12758 metrest 13976 dvef 14158 bj-charfunbi 14533 pw1nct 14722 nnsf 14724 exmidsbthrlem 14740 |
Copyright terms: Public domain | W3C validator |