Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mp3an13 | Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.) |
Ref | Expression |
---|---|
mp3an13.1 | |
mp3an13.2 | |
mp3an13.3 |
Ref | Expression |
---|---|
mp3an13 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an13.1 | . 2 | |
2 | mp3an13.2 | . . 3 | |
3 | mp3an13.3 | . . 3 | |
4 | 2, 3 | mp3an3 1316 | . 2 |
5 | 1, 4 | mpan 421 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 968 |
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 970 |
This theorem is referenced by: pitonnlem1p1 7787 mulid1 7896 addltmul 9093 eluzaddi 9492 fz01en 9988 fznatpl1 10011 expubnd 10512 bernneq 10575 bernneq2 10576 efi4p 11658 efival 11673 cos2tsin 11692 cos01bnd 11699 cos01gt0 11703 dvds0 11746 odd2np1 11810 opoe 11832 gcdid 11919 pythagtriplem4 12200 blssioo 13195 tgioo 13196 rerestcntop 13200 sinperlem 13379 sincosq1sgn 13397 sincosq2sgn 13398 sinq12gt0 13401 cosq14gt0 13403 |
Copyright terms: Public domain | W3C validator |