![]() |
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 3539 | . . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴) | |
2 | 1 | adantl 277 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴) |
3 | ifcldadc.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶) | |
4 | 2, 3 | eqeltrd 2254 | . 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶) |
5 | iffalse 3542 | . . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵) | |
6 | 5 | adantl 277 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵) |
7 | ifcldadc.2 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶) | |
8 | 6, 7 | eqeltrd 2254 | . 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶) |
9 | ifcldadc.dc | . . 3 ⊢ (𝜑 → DECID 𝜓) | |
10 | exmiddc 836 | . . 3 ⊢ (DECID 𝜓 → (𝜓 ∨ ¬ 𝜓)) | |
11 | 9, 10 | syl 14 | . 2 ⊢ (𝜑 → (𝜓 ∨ ¬ 𝜓)) |
12 | 4, 8, 11 | mpjaodan 798 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ∨ wo 708 DECID wdc 834 = wceq 1353 ∈ wcel 2148 ifcif 3534 |
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-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-dc 835 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-if 3535 |
This theorem is referenced by: updjudhf 7077 omp1eomlem 7092 difinfsnlem 7097 ctmlemr 7106 ctssdclemn0 7108 ctssdc 7111 enumctlemm 7112 xaddf 9843 xaddval 9844 iseqf1olemqcl 10485 iseqf1olemnab 10487 iseqf1olemjpcl 10494 iseqf1olemqpcl 10495 seq3f1oleml 10502 seq3f1o 10503 exp3val 10521 xrmaxiflemcl 11252 summodclem2a 11388 zsumdc 11391 fsum3 11394 isumss 11398 fsum3cvg2 11401 fsum3ser 11404 fsumcl2lem 11405 fsumadd 11413 sumsnf 11416 sumsplitdc 11439 fsummulc2 11455 isumlessdc 11503 cvgratz 11539 prodmodclem3 11582 prodmodclem2a 11583 zproddc 11586 fprodseq 11590 fprodmul 11598 prodsnf 11599 eucalgval2 12052 lcmval 12062 pcmpt 12340 ennnfonelemg 12403 mulgval 12985 mulgfng 12986 lgsval 14375 lgsfvalg 14376 lgsfcl2 14377 lgscllem 14378 lgsval2lem 14381 lgsdir 14406 lgsdilem2 14407 lgsdi 14408 lgsne0 14409 subctctexmid 14720 |
Copyright terms: Public domain | W3C validator |