![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpsyl | GIF 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: snssg 3738 relcnvtr 5160 relresfld 5170 relcoi1 5172 funco 5268 foimacnv 5491 fvi 5586 isoini2 5833 ovidig 6006 smores2 6309 tfrlem5 6329 snnen2og 6873 phpm 6879 fict 6882 infnfi 6909 isinfinf 6911 exmidpw 6922 difinfinf 7114 enumct 7128 exmidfodomrlemr 7215 exmidfodomrlemrALT 7216 isumz 11411 fsumsersdc 11417 isumclim 11443 isumclim3 11445 zprodap0 11603 alzdvds 11874 zsupcl 11962 infssuzex 11964 gcddvds 11978 dvdslegcd 11979 pclemub 12301 ennnfonelemj0 12416 ennnfonelemg 12418 ennnfonelemrn 12434 ctinf 12445 strle1g 12580 fnpr2ob 12778 metrest 14359 dvef 14541 bj-charfunbi 14916 pw1nct 15106 nnsf 15108 exmidsbthrlem 15124 |
Copyright terms: Public domain | W3C validator |