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 650 | 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 604 ax-in2 605 |
This theorem is referenced by: condandc 867 nelrdva 2919 exmid01 4159 frirrg 4310 fimax2gtrilemstep 6845 unsnfidcex 6864 unsnfidcel 6865 difinfsn 7044 nninfisollemne 7074 fodju0 7090 exmidfodomrlemr 7137 exmidfodomrlemrALT 7138 ltntri 8003 prodgt0 8723 ixxdisj 9807 icodisj 9896 iseqf1olemnab 10387 seq3f1olemqsumk 10398 ltabs 10987 divalglemnqt 11810 zsupcllemstep 11831 infssuzex 11835 sqnprm 12012 znnen 12127 dedekindeulemuub 12995 dedekindeulemlu 12999 dedekindicclemuub 13004 dedekindicclemlu 13008 ivthinclemlopn 13014 ivthinclemuopn 13016 limcimo 13034 cnplimclemle 13037 pilem3 13104 logbgcd1irraplemexp 13285 pwtrufal 13569 pwle2 13570 peano3nninf 13579 nninffeq 13592 refeq 13599 trilpolemeq1 13611 taupi 13641 |
Copyright terms: Public domain | W3C validator |