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 6826 prarloclem5 7462 ltsopr 7558 suplocsrlem 7770 nominpos 9115 ublbneg 9572 absle 11053 rexanre 11184 rexico 11185 climshftlemg 11265 serf0 11315 dvds1lem 11764 dvds2lem 11765 lmconst 13010 addcncntoplem 13345 bj-indind 13967 |
Copyright terms: Public domain | W3C validator |