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 6710 prarloclem5 7276 ltsopr 7372 suplocsrlem 7584 nominpos 8925 ublbneg 9373 absle 10829 rexanre 10960 rexico 10961 climshftlemg 11039 serf0 11089 dvds1lem 11431 dvds2lem 11432 lmconst 12312 addcncntoplem 12647 bj-indind 13057 |
Copyright terms: Public domain | W3C validator |