New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > mpdan | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.) |
Ref | Expression |
---|---|
mpdan.1 | ⊢ (φ → ψ) |
mpdan.2 | ⊢ ((φ ∧ ψ) → χ) |
Ref | Expression |
---|---|
mpdan | ⊢ (φ → χ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 ⊢ (φ → φ) | |
2 | mpdan.1 | . 2 ⊢ (φ → ψ) | |
3 | mpdan.2 | . 2 ⊢ ((φ ∧ ψ) → χ) | |
4 | 1, 2, 3 | syl2anc 642 | 1 ⊢ (φ → χ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 358 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 df-an 360 |
This theorem is referenced by: mpan2 652 mpjaodan 761 mpd3an3 1278 eueq2 3010 csbiegf 3176 difsnb 3850 ltfinp1 4462 vfinncsp 4554 addccan2 4559 fnressn 5438 f1oiso2 5500 fvdomfn 5868 fvranfn 5869 qsdisj 5995 enadj 6060 enmap2lem3 6065 enmap1lem3 6071 nclecid 6197 le0nc 6200 nnltp1c 6262 nmembers1 6271 |
Copyright terms: Public domain | W3C validator |