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 424 | 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 426 mp2and 429 rspcimedv 2786 ovig 5885 prcdnql 7285 prcunqu 7286 p1le 8600 nnge1 8736 zltp1le 9101 gtndiv 9139 uzss 9339 addlelt 9548 xrre2 9597 xrre3 9598 zltaddlt1le 9782 modfzo0difsn 10161 leexp2r 10340 expnlbnd2 10410 facavg 10485 caubnd2 10882 maxleast 10978 mulcn2 11074 cn1lem 11076 climsqz 11097 climsqz2 11098 climcvg1nlem 11111 fsumabs 11227 cvgratnnlemnexp 11286 cvgratnnlemmn 11287 zsupcllemstep 11627 gcdzeq 11699 algcvgblem 11719 algcvga 11721 lcmdvdsb 11754 coprm 11811 bldisj 12559 xblm 12575 metss2lem 12655 bdxmet 12659 limccoap 12805 |
Copyright terms: Public domain | W3C validator |