ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ifcldcd Unicode version

Theorem ifcldcd 3570
Description: Membership (closure) of a conditional operator, deduction form. (Contributed by Jim Kingdon, 8-Aug-2021.)
Hypotheses
Ref Expression
ifcldcd.a  |-  ( ph  ->  A  e.  C )
ifcldcd.b  |-  ( ph  ->  B  e.  C )
ifcldcd.dc  |-  ( ph  -> DECID  ps )
Assertion
Ref Expression
ifcldcd  |-  ( ph  ->  if ( ps ,  A ,  B )  e.  C )

Proof of Theorem ifcldcd
StepHypRef Expression
1 iftrue 3539 . . . 4  |-  ( ps 
->  if ( ps ,  A ,  B )  =  A )
21adantl 277 . . 3  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  =  A )
3 ifcldcd.a . . . 4  |-  ( ph  ->  A  e.  C )
43adantr 276 . . 3  |-  ( (
ph  /\  ps )  ->  A  e.  C )
52, 4eqeltrd 2254 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  e.  C )
6 iffalse 3542 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  A ,  B
)  =  B )
76adantl 277 . . 3  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  =  B )
8 ifcldcd.b . . . 4  |-  ( ph  ->  B  e.  C )
98adantr 276 . . 3  |-  ( (
ph  /\  -.  ps )  ->  B  e.  C )
107, 9eqeltrd 2254 . 2  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  e.  C )
11 ifcldcd.dc . . 3  |-  ( ph  -> DECID  ps )
12 df-dc 835 . . 3  |-  (DECID  ps  <->  ( ps  \/  -.  ps ) )
1311, 12sylib 122 . 2  |-  ( ph  ->  ( ps  \/  -.  ps ) )
145, 10, 13mpjaodan 798 1  |-  ( ph  ->  if ( ps ,  A ,  B )  e.  C )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    \/ wo 708  DECID wdc 834    = wceq 1353    e. 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:  fimax2gtrilemstep  6899  nnnninf  7123  nnnninfeq  7125  fodjuf  7142  fodjum  7143  fodju0  7144  mkvprop  7155  nninfwlporlemd  7169  nninfwlporlem  7170  nninfwlpoimlemg  7172  nninfwlpoimlemginf  7173  xaddf  9842  xaddval  9843  uzin2  10991  fsum3ser  11400  fsumsplit  11410  explecnv  11508  fprodsplitdc  11599  pcmpt2  12336  ennnfonelemp1  12401  opifismgmdc  12784  lgsval  14336  lgsfvalg  14337  lgsfcl2  14338  lgscllem  14339  lgsval2lem  14342  lgsneg  14356  lgsdilem  14359  lgsdir2  14365  lgsdir  14367  lgsdi  14369  lgsne0  14370  bj-charfundc  14480  nnsf  14674  peano4nninf  14675  nninfsellemcl  14680  nninffeq  14689  dceqnconst  14727  dcapnconst  14728
  Copyright terms: Public domain W3C validator