![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ifcldadc | Unicode version |
Description: Conditional closure. (Contributed by Jim Kingdon, 11-Jan-2022.) |
Ref | Expression |
---|---|
ifcldadc.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
ifcldadc.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
ifcldadc.dc |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ifcldadc |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iftrue 3539 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantl 277 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | ifcldadc.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | eqeltrd 2254 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | iffalse 3542 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 5 | adantl 277 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | ifcldadc.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 6, 7 | eqeltrd 2254 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | ifcldadc.dc |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
10 | exmiddc 836 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | 9, 10 | syl 14 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 4, 8, 11 | mpjaodan 798 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
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 9842 xaddval 9843 iseqf1olemqcl 10483 iseqf1olemnab 10485 iseqf1olemjpcl 10492 iseqf1olemqpcl 10493 seq3f1oleml 10500 seq3f1o 10501 exp3val 10519 xrmaxiflemcl 11248 summodclem2a 11384 zsumdc 11387 fsum3 11390 isumss 11394 fsum3cvg2 11397 fsum3ser 11400 fsumcl2lem 11401 fsumadd 11409 sumsnf 11412 sumsplitdc 11435 fsummulc2 11451 isumlessdc 11499 cvgratz 11535 prodmodclem3 11578 prodmodclem2a 11579 zproddc 11582 fprodseq 11586 fprodmul 11594 prodsnf 11595 eucalgval2 12047 lcmval 12057 pcmpt 12335 ennnfonelemg 12398 mulgval 12940 mulgfng 12941 lgsval 14298 lgsfvalg 14299 lgsfcl2 14300 lgscllem 14301 lgsval2lem 14304 lgsdir 14329 lgsdilem2 14330 lgsdi 14331 lgsne0 14332 subctctexmid 14632 |
Copyright terms: Public domain | W3C validator |