Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpanr1 | Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Ref | Expression |
---|---|
mpanr1.1 | |
mpanr1.2 |
Ref | Expression |
---|---|
mpanr1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpanr1.1 | . 2 | |
2 | mpanr1.2 | . . 3 | |
3 | 2 | anassrs 397 | . 2 |
4 | 1, 3 | mpanl2 431 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
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 is referenced by: mpanr12 435 axcnre 7682 rec11api 8506 divdiv23apzi 8518 recp1lt1 8650 divgt0i 8661 divge0i 8662 ltreci 8663 lereci 8664 lt2msqi 8665 le2msqi 8666 msq11i 8667 ltdiv23i 8677 ge0gtmnf 9599 sqrt11i 10897 sqrtmuli 10898 sqrtmsq2i 10900 sqrtlei 10901 sqrtlti 10902 cos01gt0 11458 |
Copyright terms: Public domain | W3C validator |