New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > mpd | GIF version |
Description: A modus ponens deduction. A translation of natural deduction rule → E (→ elimination). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
mpd.1 | ⊢ (φ → ψ) |
mpd.2 | ⊢ (φ → (ψ → χ)) |
Ref | Expression |
---|---|
mpd | ⊢ (φ → χ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpd.1 | . 2 ⊢ (φ → ψ) | |
2 | mpd.2 | . . 3 ⊢ (φ → (ψ → χ)) | |
3 | 2 | a2i 12 | . 2 ⊢ ((φ → ψ) → (φ → χ)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ (φ → χ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-2 7 |
This theorem is referenced by: syl 15 mpi 16 id 19 mpcom 32 mpdd 36 mp2d 41 pm2.43i 43 syl3c 57 pm2.21dd 99 mt2d 109 mt3d 117 mt4d 130 mpbid 201 mpbird 223 mpjaod 370 jcai 522 mp2and 660 mp3and 1280 exlimddv 1638 exlimdd 1889 eqrdav 2352 rexlimddv 2742 vtoclgft 2905 sseldd 3274 ssneldd 3276 tpid3g 3831 preq12b 4127 iota5 4359 ssfin 4470 nnpw1ex 4484 tfin11 4493 tfinpw1 4494 evenodddisj 4516 sfin112 4529 sfindbl 4530 sfintfin 4532 sfinltfin 4535 vfin1cltv 4547 vfinspsslem1 4550 vinf 4555 nulnnn 4556 phi11lem1 4595 ffvelrn 5415 dffo4 5423 f1oiso2 5500 ov6g 5600 ovmpt2x 5712 trd 5921 antid 5929 connexd 5931 weds 5938 erref 5959 mapvalg 6009 mapsn 6026 enprmaplem3 6078 nenpw1pwlem2 6085 peano4nc 6150 ncspw1eu 6159 nntccl 6170 leconnnc 6218 tlecg 6230 ce2le 6233 addcdi 6250 ncslemuc 6255 nchoicelem17 6305 nchoicelem19 6307 nchoice 6308 |
Copyright terms: Public domain | W3C validator |