![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ifcldcd | Unicode version |
Description: Membership (closure) of a conditional operator, deduction form. (Contributed by Jim Kingdon, 8-Aug-2021.) |
Ref | Expression |
---|---|
ifcldcd.a |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
ifcldcd.b |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
ifcldcd.dc |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ifcldcd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iftrue 3541 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantl 277 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | ifcldcd.a |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | adantr 276 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | eqeltrd 2254 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | iffalse 3544 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 6 | adantl 277 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | ifcldcd.b |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 8 | adantr 276 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 7, 9 | eqeltrd 2254 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | ifcldcd.dc |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
12 | df-dc 835 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
13 | 11, 12 | sylib 122 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 5, 10, 13 | 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 3537 |
This theorem is referenced by: fimax2gtrilemstep 6902 nnnninf 7126 nnnninfeq 7128 fodjuf 7145 fodjum 7146 fodju0 7147 mkvprop 7158 nninfwlporlemd 7172 nninfwlporlem 7173 nninfwlpoimlemg 7175 nninfwlpoimlemginf 7176 xaddf 9846 xaddval 9847 uzin2 10998 fsum3ser 11407 fsumsplit 11417 explecnv 11515 fprodsplitdc 11606 pcmpt2 12344 ennnfonelemp1 12409 opifismgmdc 12795 lgsval 14444 lgsfvalg 14445 lgsfcl2 14446 lgscllem 14447 lgsval2lem 14450 lgsneg 14464 lgsdilem 14467 lgsdir2 14473 lgsdir 14475 lgsdi 14477 lgsne0 14478 bj-charfundc 14599 nnsf 14793 peano4nninf 14794 nninfsellemcl 14799 nninffeq 14808 dceqnconst 14847 dcapnconst 14848 |
Copyright terms: Public domain | W3C validator |