![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm2.65da | Unicode version |
Description: Deduction for proof by contradiction. (Contributed by NM, 12-Jun-2014.) |
Ref | Expression |
---|---|
pm2.65da.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
pm2.65da.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
pm2.65da |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.65da.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ex 115 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | pm2.65da.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | ex 115 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | pm2.65d 660 |
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-ia3 108 ax-in1 614 ax-in2 615 |
This theorem is referenced by: condandc 881 nelrdva 2944 exmid01 4195 frirrg 4346 fimax2gtrilemstep 6893 unsnfidcex 6912 unsnfidcel 6913 difinfsn 7092 nninfisollemne 7122 fodju0 7138 nninfwlpoimlemginf 7167 exmidfodomrlemr 7194 exmidfodomrlemrALT 7195 ltntri 8062 prodgt0 8785 ixxdisj 9877 icodisj 9966 iseqf1olemnab 10461 seq3f1olemqsumk 10472 ltabs 11067 divalglemnqt 11895 zsupcllemstep 11916 infssuzex 11920 suprzubdc 11923 sqnprm 12106 znnen 12369 dedekindeulemuub 13728 dedekindeulemlu 13732 dedekindicclemuub 13737 dedekindicclemlu 13741 ivthinclemlopn 13747 ivthinclemuopn 13749 limcimo 13767 cnplimclemle 13770 pilem3 13837 logbgcd1irraplemexp 14019 pwtrufal 14369 pwle2 14370 peano3nninf 14379 nninffeq 14392 refeq 14399 trilpolemeq1 14411 taupi 14441 |
Copyright terms: Public domain | W3C validator |