![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm2.65i | Unicode version |
Description: Inference for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
Ref | Expression |
---|---|
pm2.65i.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
pm2.65i.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
pm2.65i |
![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.65i.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | pm2.65i.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | nsyl3 627 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | pm2.01 617 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | ax-mp 5 |
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-in1 615 ax-in2 616 |
This theorem is referenced by: mt2 641 mto 663 pm5.19 707 noel 3441 0nelop 4269 elirr 4561 en2lp 4574 soirri 5044 canth 5853 0neqopab 5945 fzp1disj 10116 fzonel 10196 fzouzdisj 10216 4sqlem17 12450 lgsval2lem 14897 bj-imnimnn 14976 nnnotnotr 15228 |
Copyright terms: Public domain | W3C validator |