![]() |
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-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: relcnvtr 4994 relresfld 5004 relcoi1 5006 funco 5099 foimacnv 5319 fvi 5410 isoini2 5652 ovidig 5820 smores2 6121 tfrlem5 6141 snnen2og 6682 phpm 6688 fict 6691 infnfi 6718 isinfinf 6720 exmidpw 6731 difinfinf 6901 enumct 6914 exmidfodomrlemr 6967 exmidfodomrlemrALT 6968 isumz 10997 fsumsersdc 11003 isumclim 11029 isumclim3 11031 alzdvds 11347 zsupcl 11435 infssuzex 11437 gcddvds 11447 dvdslegcd 11448 ennnfonelemrn 11724 ctinf 11735 strle1g 11831 metrest 12434 nnsf 12783 exmidsbthrlem 12801 |
Copyright terms: Public domain | W3C validator |