New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > mp3an1 | Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
Ref | Expression |
---|---|
mp3an1.1 | |
mp3an1.2 |
Ref | Expression |
---|---|
mp3an1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an1.1 | . 2 | |
2 | mp3an1.2 | . . 3 | |
3 | 2 | 3expb 1152 | . 2 |
4 | 1, 3 | mpan 651 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 358 w3a 934 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 177 df-an 360 df-3an 936 |
This theorem is referenced by: mp3an12 1267 mp3an1i 1270 mp3anl1 1271 mp3an 1277 opkelcokg 4261 opkelimagekg 4271 ltfintri 4466 vfinspnn 4541 vfinspclt 4552 spaccl 6284 spacind 6285 nchoicelem3 6289 nchoicelem4 6290 nchoicelem6 6292 nchoicelem9 6295 nchoicelem12 6298 nchoicelem14 6300 nchoicelem17 6303 |
Copyright terms: Public domain | W3C validator |