![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ifcldadc | GIF version |
Description: Conditional closure. (Contributed by Jim Kingdon, 11-Jan-2022.) |
Ref | Expression |
---|---|
ifcldadc.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶) |
ifcldadc.2 | ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶) |
ifcldadc.dc | ⊢ (𝜑 → DECID 𝜓) |
Ref | Expression |
---|---|
ifcldadc | ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iftrue 3484 | . . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴) | |
2 | 1 | adantl 275 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴) |
3 | ifcldadc.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶) | |
4 | 2, 3 | eqeltrd 2217 | . 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶) |
5 | iffalse 3487 | . . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵) | |
6 | 5 | adantl 275 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵) |
7 | ifcldadc.2 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶) | |
8 | 6, 7 | eqeltrd 2217 | . 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶) |
9 | ifcldadc.dc | . . 3 ⊢ (𝜑 → DECID 𝜓) | |
10 | exmiddc 822 | . . 3 ⊢ (DECID 𝜓 → (𝜓 ∨ ¬ 𝜓)) | |
11 | 9, 10 | syl 14 | . 2 ⊢ (𝜑 → (𝜓 ∨ ¬ 𝜓)) |
12 | 4, 8, 11 | mpjaodan 788 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ∨ wo 698 DECID wdc 820 = wceq 1332 ∈ wcel 1481 ifcif 3479 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-11 1485 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-dc 821 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-if 3480 |
This theorem is referenced by: updjudhf 6972 omp1eomlem 6987 difinfsnlem 6992 ctmlemr 7001 ctssdclemn0 7003 ctssdc 7006 enumctlemm 7007 xaddf 9657 xaddval 9658 iseqf1olemqcl 10290 iseqf1olemnab 10292 iseqf1olemjpcl 10299 iseqf1olemqpcl 10300 seq3f1oleml 10307 seq3f1o 10308 exp3val 10326 xrmaxiflemcl 11046 summodclem2a 11182 zsumdc 11185 fsum3 11188 isumss 11192 fsum3cvg2 11195 fsum3ser 11198 fsumcl2lem 11199 fsumadd 11207 sumsnf 11210 sumsplitdc 11233 fsummulc2 11249 isumlessdc 11297 cvgratz 11333 prodmodclem3 11376 prodmodclem2a 11377 zproddc 11380 fprodseq 11384 eucalgval2 11770 lcmval 11780 ennnfonelemg 11952 subctctexmid 13369 |
Copyright terms: Public domain | W3C validator |