Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpand | Unicode version |
Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
Ref | Expression |
---|---|
mpand.1 | |
mpand.2 |
Ref | Expression |
---|---|
mpand |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpand.1 | . 2 | |
2 | mpand.2 | . . 3 | |
3 | 2 | ancomsd 256 | . 2 |
4 | 1, 3 | mpan2d 404 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: mpani 406 mp2and 409 rspcimedv 2658 ovig 5622 prcdnql 6582 prcunqu 6583 p1le 7815 nnge1 7937 zltp1le 8298 gtndiv 8335 uzss 8493 xrre2 8734 xrre3 8735 leexp2r 9308 expnlbnd2 9374 caubnd2 9713 mulcn2 9833 cn1lem 9834 climsqz 9855 climsqz2 9856 climcvg1nlem 9868 algcvgblem 9888 ialgcvga 9890 |
Copyright terms: Public domain | W3C validator |