New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > mp2an | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.) |
Ref | Expression |
---|---|
mp2an.1 | ⊢ φ |
mp2an.2 | ⊢ ψ |
mp2an.3 | ⊢ ((φ ∧ ψ) → χ) |
Ref | Expression |
---|---|
mp2an | ⊢ χ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp2an.2 | . 2 ⊢ ψ | |
2 | mp2an.1 | . . 3 ⊢ φ | |
3 | mp2an.3 | . . 3 ⊢ ((φ ∧ ψ) → χ) | |
4 | 2, 3 | mpan 651 | . 2 ⊢ (ψ → χ) |
5 | 1, 4 | ax-mp 5 | 1 ⊢ χ |
Copyright terms: Public domain | W3C validator |