| 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 1230 |
. 2
|
| 4 | 1, 3 | mpan 424 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
| This theorem depends on definitions: df-bi 117 df-3an 1006 |
| This theorem is referenced by: mp3an12 1363 mp3an1i 1366 mp3anl1 1367 mp3an 1373 mp3an2i 1378 mp3an3an 1379 tfrlem9 6485 rdgexgg 6544 oaexg 6616 omexg 6619 oeiexg 6621 oav2 6631 nnaordex 6696 mulidnq 7609 1idpru 7811 addgt0sr 7995 muladd11 8312 cnegex 8357 negsubdi 8435 renegcl 8440 mulneg1 8574 ltaddpos 8632 addge01 8652 rimul 8765 recclap 8859 recidap 8866 recidap2 8867 recdivap2 8905 divdiv23apzi 8945 ltmul12a 9040 lemul12a 9042 mulgt1 9043 ltmulgt11 9044 gt0div 9050 ge0div 9051 ltdiv23i 9106 8th4div3 9363 gtndiv 9575 nn0ind 9594 fnn0ind 9596 xrre2 10056 ioorebasg 10210 fzen 10278 elfz0ubfz0 10360 expubnd 10859 le2sq2 10878 bernneq 10923 expnbnd 10926 faclbnd6 11007 bccl 11030 hashfacen 11101 wrdred1hash 11158 ccatlid 11184 swrd0g 11242 shftfval 11383 mulreap 11426 caucvgrelemrec 11541 binom1p 12048 efi4p 12280 sinadd 12299 cosadd 12300 cos2t 12313 cos2tsin 12314 absefib 12334 efieq1re 12335 demoivreALT 12337 odd2np1 12436 opoe 12458 omoe 12459 opeo 12460 omeo 12461 gcdadd 12558 gcdmultiple 12593 algcvgblem 12623 algcvga 12625 isprm3 12692 coprm 12718 1arith2 12943 rmodislmod 14368 cnfldneg 14590 cnfldmulg 14593 cnfldexp 14594 zringmulg 14615 zringsubgval 14622 bl2ioo 15277 ioo2blex 15279 mpomulcn 15293 sinperlem 15535 logge0 15607 lgsdir2 15765 1lgs 15775 |
| Copyright terms: Public domain | W3C validator |