![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sylan9 | GIF version |
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Ref | Expression |
---|---|
sylan9.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
sylan9.2 | ⊢ (𝜃 → (𝜒 → 𝜏)) |
Ref | Expression |
---|---|
sylan9 | ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | sylan9.2 | . . 3 ⊢ (𝜃 → (𝜒 → 𝜏)) | |
3 | 1, 2 | syl9 72 | . 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏))) |
4 | 3 | imp 123 | 1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 |
This theorem is referenced by: sbequi 1812 rspc2 2804 rspc3v 2809 copsexg 4174 chfnrn 5539 ffnfv 5586 f1elima 5682 smoel2 6208 th3q 6542 fiintim 6825 addnnnq0 7281 mulnnnq0 7282 addsrpr 7577 mulsrpr 7578 cau3lem 10918 rescncf 12776 |
Copyright terms: Public domain | W3C validator |