![]() |
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 151 stdcn 848 con4biddc 858 jaddc 865 con1biddc 877 necon4addc 2430 necon4bddc 2431 necon4ddc 2432 necon1addc 2436 necon1bddc 2437 dmcosseq 4916 iss 4971 funopg 5269 snon0 6966 metrest 14483 |
Copyright terms: Public domain | W3C validator |