![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > dcbii | Unicode version |
Description: Equivalence property for decidability. Inference form. (Contributed by Jim Kingdon, 28-Mar-2018.) |
Ref | Expression |
---|---|
dcbii.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
dcbii |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dcbii.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | dcbiit 839 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
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-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 |
This theorem depends on definitions: df-bi 117 df-dc 835 |
This theorem is referenced by: dcbi 936 dcned 2353 dfrex2dc 2468 euxfr2dc 2922 exmidexmid 4196 pw1fin 6909 dcfi 6979 elnn0dc 9609 elnndc 9610 exfzdc 10237 fprod1p 11602 nnwosdc 12034 prmdc 12124 pclemdc 12282 nninfdclemcl 12443 nninfdclemp1 12445 nninfsellemdc 14679 |
Copyright terms: Public domain | W3C validator |