![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > dcbid | GIF version |
Description: Equivalence property for decidability. Deduction form. (Contributed by Jim Kingdon, 7-Sep-2019.) |
Ref | Expression |
---|---|
dcbid.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
dcbid | ⊢ (𝜑 → (DECID 𝜓 ↔ DECID 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dcbid.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | notbid 667 | . . 3 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒)) |
3 | 1, 2 | orbi12d 793 | . 2 ⊢ (𝜑 → ((𝜓 ∨ ¬ 𝜓) ↔ (𝜒 ∨ ¬ 𝜒))) |
4 | df-dc 835 | . 2 ⊢ (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓)) | |
5 | df-dc 835 | . 2 ⊢ (DECID 𝜒 ↔ (𝜒 ∨ ¬ 𝜒)) | |
6 | 3, 4, 5 | 3bitr4g 223 | 1 ⊢ (𝜑 → (DECID 𝜓 ↔ DECID 𝜒)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 105 ∨ wo 708 DECID wdc 834 |
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: dcbiit 839 exmidexmid 4197 exmidel 4206 dcdifsnid 6505 finexdc 6902 pw1dc1 6913 undifdcss 6922 ssfirab 6933 fidcenumlemrks 6952 dcfi 6980 difinfsnlem 7098 difinfsn 7099 ctssdclemn0 7109 ctssdccl 7110 ctssdclemr 7111 ctssdc 7112 iswomni 7163 enwomnilem 7167 nninfdcinf 7169 nninfwlporlem 7171 nninfwlpoimlemdc 7175 nninfwlpoim 7176 netap 7253 ltdcpi 7322 enqdc 7360 enqdc1 7361 ltdcnq 7396 fzodcel 10152 exfzdc 10240 sumeq1 11363 sumdc 11366 summodclem2 11390 summodc 11391 zsumdc 11392 fsum3 11395 isumz 11397 isumss 11399 fisumss 11400 isumss2 11401 fsum3cvg2 11402 fsumsersdc 11403 fsumsplit 11415 prodeq1f 11560 prodmodclem2a 11584 prodmodclem2 11585 prodmodc 11586 zproddc 11587 fprodseq 11591 prod1dc 11594 prodssdc 11597 fprodssdc 11598 fprodsplitdc 11604 dvdsdc 11805 zdvdsdc 11819 zsupcllemstep 11946 infssuzex 11950 suprzubdc 11953 nninfdcex 11954 zsupssdc 11955 nnmindc 12035 nnminle 12036 uzwodc 12038 nnwosdc 12040 hashdvds 12221 eulerthlemfi 12228 phisum 12240 infpnlem2 12358 1arith 12365 ennnfonelemr 12424 ennnfonelemim 12425 ctinf 12431 ctiunctlemudc 12438 ctiunct 12441 ssomct 12446 ssnnctlemct 12447 nninfdclemcl 12449 nninfdclemp1 12451 lgsval 14408 lgsfvalg 14409 lgsfcl2 14410 lgsval2lem 14414 lgsdir2 14437 lgsne0 14442 sumdc2 14554 bj-charfundcALT 14564 bj-charfunbi 14566 nninfsellemdc 14762 iswomninnlem 14800 iswomni0 14802 redcwlpo 14806 redc0 14808 reap0 14809 dceqnconst 14810 dcapnconst 14811 |
Copyright terms: Public domain | W3C validator |