Theorem ifcldcd 3550

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

Step	Hyp	Ref	Expression
1		iftrue 3520	. . . 4 |- ( ps -> if ( ps , A , B ) = A )
2	1	adantl 275	. . 3 |- ( ( ph /\ ps ) -> if ( ps , A , B ) = A )
3		ifcldcd.a	. . . 4 |- ( ph -> A e. C )
4	3	adantr 274	. . 3 |- ( ( ph /\ ps ) -> A e. C )
5	2, 4	eqeltrd 2241	. 2 |- ( ( ph /\ ps ) -> if ( ps , A , B ) e. C )
6		iffalse 3523	. . . 4 |- ( -. ps -> if ( ps , A , B ) = B )
7	6	adantl 275	. . 3 |- ( ( ph /\ -. ps ) -> if ( ps , A , B ) = B )
8		ifcldcd.b	. . . 4 |- ( ph -> B e. C )
9	8	adantr 274	. . 3 |- ( ( ph /\ -. ps ) -> B e. C )
10	7, 9	eqeltrd 2241	. 2 |- ( ( ph /\ -. ps ) -> if ( ps , A , B ) e. C )
11		ifcldcd.dc	. . 3 |- ( ph -> DECID ps )
12		df-dc 825	. . 3 |- (DECID ps <-> ( ps \/ -. ps ) )
13	11, 12	sylib 121	. 2 |- ( ph -> ( ps \/ -. ps ) )
14	5, 10, 13	mpjaodan 788	1 |- ( ph -> if ( ps , A , B ) e. C )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   \/ wo 698  DECID wdc 824   = wceq 1342   e. wcel 2135   ifcif 3515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-11 1493  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-dc 825  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-if 3516

This theorem is referenced by:  fimax2gtrilemstep  6857  nnnninf  7081  nnnninfeq  7083  fodjuf  7100  fodjum  7101  fodju0  7102  mkvprop  7113  xaddf  9771  xaddval  9772  uzin2  10915  fsum3ser  11324  fsumsplit  11334  explecnv  11432  fprodsplitdc  11523  pcmpt2  12251  ennnfonelemp1  12276  bj-charfundc  13525  nnsf  13719  peano4nninf  13720  nninfsellemcl  13725  nninffeq  13734  dceqnconst  13772  dcapnconst  13773