![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl3an2 | GIF version |
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
Ref | Expression |
---|---|
syl3an2.1 | ⊢ (φ → χ) |
syl3an2.2 | ⊢ ((ψ ∧ χ ∧ θ) → τ) |
Ref | Expression |
---|---|
syl3an2 | ⊢ ((ψ ∧ φ ∧ θ) → τ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3an2.1 | . . 3 ⊢ (φ → χ) | |
2 | syl3an2.2 | . . . 4 ⊢ ((ψ ∧ χ ∧ θ) → τ) | |
3 | 2 | 3exp 1102 | . . 3 ⊢ (ψ → (χ → (θ → τ))) |
4 | 1, 3 | syl5 28 | . 2 ⊢ (ψ → (φ → (θ → τ))) |
5 | 4 | 3imp 1097 | 1 ⊢ ((ψ ∧ φ ∧ θ) → τ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 884 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 df-3an 886 |
This theorem is referenced by: syl3an2b 1171 syl3an2br 1174 syl3anl2 1183 nndi 6004 nnmass 6005 prarloclemarch2 6402 1idprl 6566 1idpru 6567 recexprlem1ssl 6605 recexprlem1ssu 6606 msqge0 7400 mulge0 7403 divsubdirap 7466 divdiv32ap 7478 peano2uz 8302 fzoshftral 8864 expdivap 8959 redivap 9102 imdivap 9109 |
Copyright terms: Public domain | W3C validator |