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 267 | . 2 |
4 | 1, 3 | mpan2d 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: mpani 427 mp2and 430 rspcimedv 2827 ovig 5954 prcdnql 7416 prcunqu 7417 p1le 8735 nnge1 8871 zltp1le 9236 gtndiv 9277 uzss 9477 addlelt 9695 xrre2 9748 xrre3 9749 zltaddlt1le 9934 modfzo0difsn 10320 leexp2r 10499 expnlbnd2 10569 facavg 10648 caubnd2 11045 maxleast 11141 mulcn2 11239 cn1lem 11241 climsqz 11262 climsqz2 11263 climcvg1nlem 11276 fsumabs 11392 cvgratnnlemnexp 11451 cvgratnnlemmn 11452 zsupcllemstep 11863 gcdzeq 11940 algcvgblem 11960 algcvga 11962 lcmdvdsb 11995 coprm 12055 pclemub 12198 bldisj 12948 xblm 12964 metss2lem 13044 bdxmet 13048 limccoap 13194 |
Copyright terms: Public domain | W3C validator |