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 3530 | . . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴) | |
2 | 1 | adantl 275 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴) |
3 | ifcldadc.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶) | |
4 | 2, 3 | eqeltrd 2247 | . 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶) |
5 | iffalse 3533 | . . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵) | |
6 | 5 | adantl 275 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵) |
7 | ifcldadc.2 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶) | |
8 | 6, 7 | eqeltrd 2247 | . 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶) |
9 | ifcldadc.dc | . . 3 ⊢ (𝜑 → DECID 𝜓) | |
10 | exmiddc 831 | . . 3 ⊢ (DECID 𝜓 → (𝜓 ∨ ¬ 𝜓)) | |
11 | 9, 10 | syl 14 | . 2 ⊢ (𝜑 → (𝜓 ∨ ¬ 𝜓)) |
12 | 4, 8, 11 | mpjaodan 793 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ∨ wo 703 DECID wdc 829 = wceq 1348 ∈ wcel 2141 ifcif 3525 |
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 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-11 1499 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-dc 830 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-if 3526 |
This theorem is referenced by: updjudhf 7052 omp1eomlem 7067 difinfsnlem 7072 ctmlemr 7081 ctssdclemn0 7083 ctssdc 7086 enumctlemm 7087 xaddf 9788 xaddval 9789 iseqf1olemqcl 10429 iseqf1olemnab 10431 iseqf1olemjpcl 10438 iseqf1olemqpcl 10439 seq3f1oleml 10446 seq3f1o 10447 exp3val 10465 xrmaxiflemcl 11195 summodclem2a 11331 zsumdc 11334 fsum3 11337 isumss 11341 fsum3cvg2 11344 fsum3ser 11347 fsumcl2lem 11348 fsumadd 11356 sumsnf 11359 sumsplitdc 11382 fsummulc2 11398 isumlessdc 11446 cvgratz 11482 prodmodclem3 11525 prodmodclem2a 11526 zproddc 11529 fprodseq 11533 fprodmul 11541 prodsnf 11542 eucalgval2 11994 lcmval 12004 pcmpt 12282 ennnfonelemg 12345 lgsval 13658 lgsfvalg 13659 lgsfcl2 13660 lgscllem 13661 lgsval2lem 13664 lgsdir 13689 lgsdilem2 13690 lgsdi 13691 lgsne0 13692 subctctexmid 13994 |
Copyright terms: Public domain | W3C validator |