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

Theorem ifcldcd 3572
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 3541 . . . 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 3544 . . . 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 3536
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