![]() |
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 1145 |
. 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 927 |
This theorem is referenced by: mp3an12 1264 mp3an1i 1267 mp3anl1 1268 mp3an 1274 mp3an2i 1279 mp3an3an 1280 tfrlem9 6100 rdgexgg 6159 oaexg 6225 omexg 6228 oeiexg 6230 oav2 6240 nnaordex 6302 mulidnq 7011 1idpru 7213 addgt0sr 7384 muladd11 7678 cnegex 7723 negsubdi 7801 renegcl 7806 mulneg1 7936 ltaddpos 7993 addge01 8013 rimul 8125 recclap 8209 recidap 8216 recidap2 8217 recdivap2 8255 divdiv23apzi 8295 ltmul12a 8384 lemul12a 8386 mulgt1 8387 ltmulgt11 8388 gt0div 8394 ge0div 8395 ltdiv23i 8450 8th4div3 8698 gtndiv 8904 nn0ind 8923 fnn0ind 8925 xrre2 9346 ioorebasg 9456 fzen 9520 elfz0ubfz0 9599 expubnd 10075 le2sq2 10093 bernneq 10137 expnbnd 10140 faclbnd6 10215 bccl 10238 hashfacen 10304 shftfval 10318 mulreap 10361 caucvgrelemrec 10475 binom1p 10942 efi4p 11071 sinadd 11090 cosadd 11091 cos2t 11104 cos2tsin 11105 absefib 11123 efieq1re 11124 demoivreALT 11126 odd2np1 11214 opoe 11236 omoe 11237 opeo 11238 omeo 11239 gcdadd 11317 gcdmultiple 11350 algcvgblem 11372 algcvga 11374 isprm3 11441 coprm 11464 |
Copyright terms: Public domain | W3C validator |