![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sylcom | GIF version |
Description: Syllogism inference with commutation of antecedents. (Contributed by NM, 29-Aug-2004.) (Proof shortened by O'Cat, 2-Feb-2006.) (Proof shortened by Stefan Allan, 23-Feb-2006.) |
Ref | Expression |
---|---|
sylcom.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
sylcom.2 | ⊢ (𝜓 → (𝜒 → 𝜃)) |
Ref | Expression |
---|---|
sylcom | ⊢ (𝜑 → (𝜓 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylcom.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | sylcom.2 | . . 3 ⊢ (𝜓 → (𝜒 → 𝜃)) | |
3 | 2 | a2i 11 | . 2 ⊢ ((𝜓 → 𝜒) → (𝜓 → 𝜃)) |
4 | 1, 3 | syl 14 | 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: syl5com 29 syl6 33 syli 37 mpbidi 150 stdcn 833 con4biddc 843 jaddc 850 con1biddc 862 necon4addc 2379 necon4bddc 2380 necon4ddc 2381 necon1addc 2385 necon1bddc 2386 dmcosseq 4818 iss 4873 funopg 5165 snon0 6832 metrest 12714 |
Copyright terms: Public domain | W3C validator |