Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mp3an23 | Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.) |
Ref | Expression |
---|---|
mp3an23.1 | |
mp3an23.2 | |
mp3an23.3 |
Ref | Expression |
---|---|
mp3an23 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an23.1 | . 2 | |
2 | mp3an23.2 | . . 3 | |
3 | mp3an23.3 | . . 3 | |
4 | 2, 3 | mp3an3 1289 | . 2 |
5 | 1, 4 | mpan2 421 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 949 |
This theorem is referenced by: sbciegf 2912 ac6sfi 6760 dju0en 7038 1qec 7164 ltaddnq 7183 halfnqq 7186 1idsr 7544 pn0sr 7547 ltm1sr 7553 muleqadd 8397 halfcl 8914 rehalfcl 8915 half0 8916 2halves 8917 halfpos2 8918 halfnneg2 8920 halfaddsub 8922 nneoor 9121 zeo 9124 fztp 9826 modqfrac 10078 iexpcyc 10365 bcn2 10478 bcpasc 10480 imre 10591 reim 10592 crim 10598 addcj 10631 imval2 10634 sinf 11338 efi4p 11351 resin4p 11352 recos4p 11353 sinneg 11360 efival 11366 cosadd 11371 sinmul 11378 sinbnd 11386 cosbnd 11387 ef01bndlem 11390 sin01bnd 11391 cos01bnd 11392 sin01gt0 11395 cos01gt0 11396 sin02gt0 11397 odd2np1lem 11496 odd2np1 11497 mopnex 12601 sincosq1lem 12833 sincosq2sgn 12835 sincosq3sgn 12836 sincosq4sgn 12837 sinq12gt0 12838 abssinper 12854 coskpi 12856 |
Copyright terms: Public domain | W3C validator |