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 655 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 ax-in1 609 ax-in2 610 |
This theorem is referenced by: condandc 876 nelrdva 2937 exmid01 4184 frirrg 4335 fimax2gtrilemstep 6878 unsnfidcex 6897 unsnfidcel 6898 difinfsn 7077 nninfisollemne 7107 fodju0 7123 nninfwlpoimlemginf 7152 exmidfodomrlemr 7179 exmidfodomrlemrALT 7180 ltntri 8047 prodgt0 8768 ixxdisj 9860 icodisj 9949 iseqf1olemnab 10444 seq3f1olemqsumk 10455 ltabs 11051 divalglemnqt 11879 zsupcllemstep 11900 infssuzex 11904 suprzubdc 11907 sqnprm 12090 znnen 12353 dedekindeulemuub 13389 dedekindeulemlu 13393 dedekindicclemuub 13398 dedekindicclemlu 13402 ivthinclemlopn 13408 ivthinclemuopn 13410 limcimo 13428 cnplimclemle 13431 pilem3 13498 logbgcd1irraplemexp 13680 pwtrufal 14030 pwle2 14031 peano3nninf 14040 nninffeq 14053 refeq 14060 trilpolemeq1 14072 taupi 14102 |
Copyright terms: Public domain | W3C validator |