Theorem ifclda 4563

Description: Conditional closure. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
ifclda.1	⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
ifclda.2	⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)

Assertion

Ref	Expression
ifclda	⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Proof of Theorem ifclda

Step	Hyp	Ref	Expression
1		iftrue 4534	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 483	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifclda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2834	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5		iffalse 4537	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 483	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifclda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
8	6, 7	eqeltrd 2834	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
9	4, 8	pm2.61dan 812	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ifcif 4528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4529

This theorem is referenced by:  unxpdomlem3  9249  updjudhf  9923  acndom  10043  iunfictbso  10106  dfac12lem2  10136  ttukeylem6  10506  canthp1lem2  10645  xaddf  13200  xmulf  13248  ccatcl  14521  swrdcl  14592  ccatco  14783  lo1bdd2  15465  o1lo1  15478  sadadd2lem2  16388  sadcaddlem  16395  sadadd2lem  16397  sadadd3  16399  lcmfval  16555  iserodd  16765  prmreclem2  16847  prmreclem4  16849  prmreclem6  16851  prmrec  16852  vdwlem6  16916  mreexexd  17589  smndex2hbas  18794  symgextf  19280  pmtrf  19318  odfval  19395  cyggex2  19760  dprdfid  19882  dmdprdsplitlem  19902  sdrgacs  20410  cygznlem1  21114  cygznlem2a  21115  cygznlem3  21117  cygth  21119  fvmptnn04if  22343  chfacfisf  22348  chfacfisfcpmat  22349  ptpjpre2  23076  ptopn2  23080  ptpjopn  23108  iccpnfcnv  24452  xrhmeo  24454  cmetcaulem  24797  ovolunlem1a  25005  ovolunlem1  25006  ioorf  25082  mbfi1fseqlem3  25227  mbfi1flim  25233  itg2seq  25252  itg2splitlem  25258  itg2split  25259  iblss  25314  itgle  25319  itgeqa  25323  ibladdlem  25329  itgaddlem1  25332  iblabslem  25337  iblabs  25338  iblabsr  25339  iblmulc2  25340  itgmulc2lem1  25341  bddmulibl  25348  bddiblnc  25351  itggt0  25353  itgcn  25354  ellimc2  25386  limccnp  25400  limccnp2  25401  dvcobr  25455  lhop1  25523  elplyd  25708  coeeq2  25748  dvply1  25789  aalioulem3  25839  dvtaylp  25874  dvradcnv  25925  psercnlem1  25929  logcnlem2  26143  logcnlem3  26144  logcnlem4  26145  logtayllem  26159  logtayl  26160  cxpcl  26174  recxpcl  26175  leibpilem2  26436  leibpi  26437  rlimcnp2  26461  efrlim  26464  igamf  26545  igamcl  26546  pclogsum  26708  dchrelbasd  26732  lgsfcl2  26796  lgscllem  26797  lgsval2lem  26800  lgsne0  26828  2sqnn0  26931  dchrvmasumiflem2  26995  dchrisum0flblem1  27001  pntrlog2bndlem4  27073  pntrlog2bndlem5  27074  pntlemj  27096  padicabv  27123  crctcshwlkn0  29065  sgnsval  32308  gsummoncoe1fzo  32657  xrge0iifcnv  32902  xrge0iifhom  32906  pnfneige0  32920  esumpinfval  33060  sigaclfu2  33108  ballotlemsv  33497  ballotlemsdom  33499  signswmnd  33557  signsvvf  33579  signsvfn  33582  mrsubcv  34490  mrsubff  34492  mrsubrn  34493  mrsubccat  34498  gg-dvcobr  35165  unblimceq0lem  35371  ptrecube  36477  poimirlem24  36501  itg2addnclem2  36529  itg2gt0cn  36532  ibladdnclem  36533  itgaddnclem1  36535  iblabsnclem  36540  iblabsnc  36541  iblmulc2nc  36542  itgmulc2nclem1  36543  itggt0cn  36547  ftc1anclem5  36554  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  areacirc  36570  cdleme27cl  39226  selvcllem5  41152  selvvvval  41155  dffltz  41373  cantnfub  42057  climsuse  44311  lptioo1  44335  icccncfext  44590  cncfiooicclem1  44596  iblsplit  44669  dirkerval2  44797  dirkerre  44798  fourierdlem9  44819  fourierdlem17  44827  fourierdlem43  44853  etransclem3  44940  etransclem7  44944  etransclem10  44947  etransclem21  44958  lincext1  47089