![]() |
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 2845 ovig 5998 prcdnql 7485 prcunqu 7486 p1le 8808 nnge1 8944 zltp1le 9309 gtndiv 9350 uzss 9550 addlelt 9770 xrre2 9823 xrre3 9824 zltaddlt1le 10009 modfzo0difsn 10397 leexp2r 10576 expnlbnd2 10648 facavg 10728 caubnd2 11128 maxleast 11224 mulcn2 11322 cn1lem 11324 climsqz 11345 climsqz2 11346 climcvg1nlem 11359 fsumabs 11475 cvgratnnlemnexp 11534 cvgratnnlemmn 11535 zsupcllemstep 11948 gcdzeq 12025 algcvgblem 12051 algcvga 12053 lcmdvdsb 12086 coprm 12146 pclemub 12289 bldisj 13940 xblm 13956 metss2lem 14036 bdxmet 14040 limccoap 14186 lgsne0 14478 |
Copyright terms: Public domain | W3C validator |