Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpani | Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.) |
Ref | Expression |
---|---|
mpani.1 | |
mpani.2 |
Ref | Expression |
---|---|
mpani |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpani.1 | . . 3 | |
2 | 1 | a1i 9 | . 2 |
3 | mpani.2 | . 2 | |
4 | 2, 3 | mpand 425 | 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 depends on definitions: df-bi 116 |
This theorem is referenced by: mp2ani 428 mulgt1 8621 recgt1i 8656 recreclt 8658 nngt0 8745 nnrecgt0 8758 elnnnn0c 9022 elnnz1 9077 recnz 9144 uz3m2nn 9368 ledivge1le 9513 expubnd 10350 expnbnd 10415 expnlbnd 10416 sin02gt0 11470 oddge22np1 11578 dvdsnprmd 11806 sinq12gt0 12911 |
Copyright terms: Public domain | W3C validator |