![]() |
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 113 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | pm2.65da.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | ex 113 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | pm2.65d 621 |
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 106 ax-in1 579 ax-in2 580 |
This theorem is referenced by: condandc 813 nelrdva 2822 exmid01 4032 frirrg 4177 fimax2gtrilemstep 6616 unsnfidcex 6630 unsnfidcel 6631 fodjuomnilem0 6802 exmidfodomrlemr 6828 exmidfodomrlemrALT 6829 prodgt0 8313 ixxdisj 9321 icodisj 9409 iseqf1olemnab 9917 seq3f1olemqsumk 9928 ltabs 10520 divalglemnqt 11198 zsupcllemstep 11219 infssuzex 11223 sqnprm 11395 znnen 11489 peano3nninf 11897 |
Copyright terms: Public domain | W3C validator |