Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE 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 1105 | . 2 |
4 | 1, 3 | mpan 400 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 w3a 885 |
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 887 |
This theorem is referenced by: mp3an12 1222 mp3an1i 1225 mp3anl1 1226 mp3an 1232 tfrlem9 5935 rdgexgg 5965 oaexg 6028 omexg 6031 oeiexg 6033 oav2 6043 nnaordex 6100 mulidnq 6487 1idpru 6689 addgt0sr 6860 muladd11 7146 cnegex 7189 negsubdi 7267 renegcl 7272 mulneg1 7392 ltaddpos 7447 addge01 7467 rimul 7576 recclap 7658 recidap 7665 recidap2 7666 recdivap2 7701 divdiv23apzi 7741 ltmul12a 7826 lemul12a 7828 mulgt1 7829 ltmulgt11 7830 gt0div 7836 ge0div 7837 ltdiv23i 7892 8th4div3 8144 gtndiv 8335 nn0ind 8352 fnn0ind 8354 xrre2 8734 ioorebasg 8844 fzen 8907 elfz0ubfz0 8982 frec2uzzd 9186 frec2uzsucd 9187 expubnd 9311 le2sq2 9329 bernneq 9369 expnbnd 9372 shftfval 9422 mulreap 9464 caucvgrelemrec 9578 algcvgblem 9888 ialgcvga 9890 |
Copyright terms: Public domain | W3C validator |