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 8589 recgt1i 8624 recreclt 8626 nngt0 8713 nnrecgt0 8726 elnnnn0c 8990 elnnz1 9045 recnz 9112 uz3m2nn 9336 ledivge1le 9481 expubnd 10318 expnbnd 10383 expnlbnd 10384 sin02gt0 11397 oddge22np1 11505 dvdsnprmd 11733 sinq12gt0 12838 |
Copyright terms: Public domain | W3C validator |