Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl6an | GIF version |
Description: A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011.) |
Ref | Expression |
---|---|
syl6an.1 | ⊢ (𝜑 → 𝜓) |
syl6an.2 | ⊢ (𝜑 → (𝜒 → 𝜃)) |
syl6an.3 | ⊢ ((𝜓 ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
syl6an | ⊢ (𝜑 → (𝜒 → 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6an.2 | . . 3 ⊢ (𝜑 → (𝜒 → 𝜃)) | |
2 | syl6an.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | jctild 314 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 ∧ 𝜃))) |
4 | syl6an.3 | . 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜏) | |
5 | 3, 4 | syl6 33 | 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-ia3 107 |
This theorem is referenced by: mapxpen 6805 prarloclem5 7432 ltsopr 7528 suplocsrlem 7740 nominpos 9085 ublbneg 9542 absle 11017 rexanre 11148 rexico 11149 climshftlemg 11229 serf0 11279 dvds1lem 11728 dvds2lem 11729 lmconst 12757 addcncntoplem 13092 bj-indind 13649 |
Copyright terms: Public domain | W3C validator |