![]() |
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 269 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpan2d 428 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: mpani 430 mp2and 433 rspcimedv 2843 ovig 5995 prcdnql 7482 prcunqu 7483 p1le 8804 nnge1 8940 zltp1le 9305 gtndiv 9346 uzss 9546 addlelt 9766 xrre2 9819 xrre3 9820 zltaddlt1le 10005 modfzo0difsn 10392 leexp2r 10571 expnlbnd2 10642 facavg 10721 caubnd2 11121 maxleast 11217 mulcn2 11315 cn1lem 11317 climsqz 11338 climsqz2 11339 climcvg1nlem 11352 fsumabs 11468 cvgratnnlemnexp 11527 cvgratnnlemmn 11528 zsupcllemstep 11940 gcdzeq 12017 algcvgblem 12043 algcvga 12045 lcmdvdsb 12078 coprm 12138 pclemub 12281 bldisj 13794 xblm 13810 metss2lem 13890 bdxmet 13894 limccoap 14040 lgsne0 14332 |
Copyright terms: Public domain | W3C validator |