![]() |
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 1147 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpan 416 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 929 |
This theorem is referenced by: mp3an12 1270 mp3an1i 1273 mp3anl1 1274 mp3an 1280 mp3an2i 1285 mp3an3an 1286 tfrlem9 6122 rdgexgg 6181 oaexg 6249 omexg 6252 oeiexg 6254 oav2 6264 nnaordex 6326 mulidnq 7045 1idpru 7247 addgt0sr 7418 muladd11 7712 cnegex 7757 negsubdi 7835 renegcl 7840 mulneg1 7970 ltaddpos 8027 addge01 8047 rimul 8159 recclap 8243 recidap 8250 recidap2 8251 recdivap2 8289 divdiv23apzi 8329 ltmul12a 8418 lemul12a 8420 mulgt1 8421 ltmulgt11 8422 gt0div 8428 ge0div 8429 ltdiv23i 8484 8th4div3 8733 gtndiv 8940 nn0ind 8959 fnn0ind 8961 xrre2 9387 ioorebasg 9541 fzen 9606 elfz0ubfz0 9685 expubnd 10143 le2sq2 10161 bernneq 10205 expnbnd 10208 faclbnd6 10283 bccl 10306 hashfacen 10372 shftfval 10386 mulreap 10429 caucvgrelemrec 10543 binom1p 11044 efi4p 11173 sinadd 11192 cosadd 11193 cos2t 11206 cos2tsin 11207 absefib 11225 efieq1re 11226 demoivreALT 11228 odd2np1 11316 opoe 11338 omoe 11339 opeo 11340 omeo 11341 gcdadd 11419 gcdmultiple 11452 algcvgblem 11474 algcvga 11476 isprm3 11543 coprm 11566 bl2ioo 12332 ioo2blex 12334 |
Copyright terms: Public domain | W3C validator |