Theorem ifcldadc 3467

Description: Conditional closure. (Contributed by Jim Kingdon, 11-Jan-2022.)

Hypotheses

Ref	Expression
ifcldadc.1	|- ( ( ph /\ ps ) -> A e. C )
ifcldadc.2	|- ( ( ph /\ -. ps ) -> B e. C )
ifcldadc.dc	|- ( ph -> DECID ps )

Assertion

Ref	Expression
ifcldadc	|- ( ph -> if ( ps , A , B ) e. C )

Proof of Theorem ifcldadc

Step	Hyp	Ref	Expression
1		iftrue 3445	. . . 4 |- ( ps -> if ( ps , A , B ) = A )
2	1	adantl 273	. . 3 |- ( ( ph /\ ps ) -> if ( ps , A , B ) = A )
3		ifcldadc.1	. . 3 |- ( ( ph /\ ps ) -> A e. C )
4	2, 3	eqeltrd 2191	. 2 |- ( ( ph /\ ps ) -> if ( ps , A , B ) e. C )
5		iffalse 3448	. . . 4 |- ( -. ps -> if ( ps , A , B ) = B )
6	5	adantl 273	. . 3 |- ( ( ph /\ -. ps ) -> if ( ps , A , B ) = B )
7		ifcldadc.2	. . 3 |- ( ( ph /\ -. ps ) -> B e. C )
8	6, 7	eqeltrd 2191	. 2 |- ( ( ph /\ -. ps ) -> if ( ps , A , B ) e. C )
9		ifcldadc.dc	. . 3 |- ( ph -> DECID ps )
10		exmiddc 804	. . 3 |- (DECID ps -> ( ps \/ -. ps ) )
11	9, 10	syl 14	. 2 |- ( ph -> ( ps \/ -. ps ) )
12	4, 8, 11	mpjaodan 770	1 |- ( ph -> if ( ps , A , B ) e. C )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   \/ wo 680  DECID wdc 802   = wceq 1314   e. wcel 1463   ifcif 3440

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-dc 803  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-if 3441

This theorem is referenced by:  updjudhf  6916  omp1eomlem  6931  difinfsnlem  6936  ctmlemr  6945  ctssdclemn0  6947  ctssdc  6950  enumctlemm  6951  xaddf  9520  xaddval  9521  iseqf1olemqcl  10152  iseqf1olemnab  10154  iseqf1olemjpcl  10161  iseqf1olemqpcl  10162  seq3f1oleml  10169  seq3f1o  10170  exp3val  10188  xrmaxiflemcl  10906  summodclem2a  11042  zsumdc  11045  fsum3  11048  isumss  11052  fsum3cvg2  11055  fsum3ser  11058  fsumcl2lem  11059  fsumadd  11067  sumsnf  11070  sumsplitdc  11093  fsummulc2  11109  isumlessdc  11157  cvgratz  11193  eucalgval2  11580  lcmval  11590  ennnfonelemg  11761  subctctexmid  12888