![]() |
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 114 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | pm2.65da.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | ex 114 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | pm2.65d 622 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 107 ax-in1 580 ax-in2 581 |
This theorem is referenced by: condandc 814 nelrdva 2823 exmid01 4038 frirrg 4186 fimax2gtrilemstep 6670 unsnfidcex 6684 unsnfidcel 6685 fodjuomnilem0 6863 exmidfodomrlemr 6889 exmidfodomrlemrALT 6890 prodgt0 8374 ixxdisj 9382 icodisj 9470 iseqf1olemnab 9978 seq3f1olemqsumk 9989 ltabs 10581 divalglemnqt 11259 zsupcllemstep 11280 infssuzex 11284 sqnprm 11456 znnen 11550 peano3nninf 12169 |
Copyright terms: Public domain | W3C validator |