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 1811 rspc2 2795 rspc3v 2800 copsexg 4161 chfnrn 5524 ffnfv 5571 f1elima 5667 smoel2 6193 th3q 6527 fiintim 6810 addnnnq0 7250 mulnnnq0 7251 addsrpr 7546 mulsrpr 7547 cau3lem 10879 rescncf 12726 |
Copyright terms: Public domain | W3C validator |