![]() |
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 3418 | . . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴) | |
2 | 1 | adantl 272 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴) |
3 | ifcldadc.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶) | |
4 | 2, 3 | eqeltrd 2171 | . 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶) |
5 | iffalse 3421 | . . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵) | |
6 | 5 | adantl 272 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵) |
7 | ifcldadc.2 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶) | |
8 | 6, 7 | eqeltrd 2171 | . 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶) |
9 | ifcldadc.dc | . . 3 ⊢ (𝜑 → DECID 𝜓) | |
10 | exmiddc 785 | . . 3 ⊢ (DECID 𝜓 → (𝜓 ∨ ¬ 𝜓)) | |
11 | 9, 10 | syl 14 | . 2 ⊢ (𝜑 → (𝜓 ∨ ¬ 𝜓)) |
12 | 4, 8, 11 | mpjaodan 750 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ∨ wo 667 DECID wdc 783 = wceq 1296 ∈ wcel 1445 ifcif 3413 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in2 583 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-11 1449 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-dc 784 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-if 3414 |
This theorem is referenced by: updjudhf 6850 ctmlemr 6870 enumctlemm 6872 xaddf 9410 xaddval 9411 iseqf1olemqcl 10036 iseqf1olemnab 10038 iseqf1olemjpcl 10045 iseqf1olemqpcl 10046 seq3f1oleml 10053 seq3f1o 10054 exp3val 10072 xrmaxiflemcl 10788 summodclem2a 10924 zsumdc 10927 fsum3 10930 isumss 10934 fsum3cvg2 10937 fsum3ser 10940 fsumcl2lem 10941 fsumadd 10949 sumsnf 10952 sumsplitdc 10975 fsummulc2 10991 isumlessdc 11039 cvgratz 11075 eucalgval2 11462 lcmval 11472 |
Copyright terms: Public domain | W3C validator |