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 398 | . 2 |
4 | 1, 3 | mpanl2 432 | 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 436 axcnre 7813 rec11api 8640 divdiv23apzi 8652 recp1lt1 8785 divgt0i 8796 divge0i 8797 ltreci 8798 lereci 8799 lt2msqi 8800 le2msqi 8801 msq11i 8802 ltdiv23i 8812 ge0gtmnf 9750 sqrt11i 11060 sqrtmuli 11061 sqrtmsq2i 11063 sqrtlei 11064 sqrtlti 11065 cos01gt0 11689 |
Copyright terms: Public domain | W3C validator |