![]() |
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-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: relcnvtr 5016 relresfld 5026 relcoi1 5028 funco 5121 foimacnv 5341 fvi 5432 isoini2 5674 ovidig 5842 smores2 6145 tfrlem5 6165 snnen2og 6706 phpm 6712 fict 6715 infnfi 6742 isinfinf 6744 exmidpw 6755 difinfinf 6938 enumct 6952 exmidfodomrlemr 7006 exmidfodomrlemrALT 7007 isumz 11050 fsumsersdc 11056 isumclim 11082 isumclim3 11084 alzdvds 11400 zsupcl 11488 infssuzex 11490 gcddvds 11500 dvdslegcd 11501 ennnfonelemrn 11777 ctinf 11788 strle1g 11892 metrest 12495 nnsf 12891 exmidsbthrlem 12909 |
Copyright terms: Public domain | W3C validator |