![]() |
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-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: syl5com 29 syl6 33 syli 37 mpbidi 149 con4biddc 792 jaddc 799 con1biddc 808 necon4addc 2325 necon4bddc 2326 necon4ddc 2327 necon1addc 2331 necon1bddc 2332 dmcosseq 4704 iss 4758 funopg 5048 snon0 6643 |
Copyright terms: Public domain | W3C validator |