Theorem ifclda 4518

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 4488	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 487	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifclda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2860	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5		iffalse 4491	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 487	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifclda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
8	6, 7	eqeltrd 2860	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
9	4, 8	pm2.61dan 825	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4483

This theorem is used by:  unxpdomlem3  9228  updjudhf  9936  acndom  10054  iunfictbso  10117  dfac12lem2  10147  ttukeylem6  10516  canthp1lem2  10662  xaddf  13276  xmulf  13324  ccatcl  14639  swrdcl  14713  ccatco  14906  lo1bdd2  15611  o1lo1  15624  sadadd2lem2  16540  sadcaddlem  16547  sadadd2lem  16549  sadadd3  16551  lcmfval  16711  iserodd  16927  prmreclem2  17009  prmreclem4  17011  prmreclem6  17013  prmrec  17014  vdwlem6  17078  mreexexd  17736  smndex2hbas  19028  symgextf  19544  pmtrf  19582  odfval  19659  cyggex2  20024  dprdfid  20146  dmdprdsplitlem  20166  sdrgacs  20967  cygznlem1  21779  cygznlem2a  21780  cygznlem3  21782  cygth  21784  selvcllem5  22355  selvvvval  22358  fvmptnn04if  23074  chfacfisf  23079  chfacfisfcpmat  23080  ptpjpre2  23806  ptopn2  23810  ptpjopn  23838  iccpnfcnv  25172  xrhmeo  25174  cmetcaulem  25516  ovolunlem1a  25724  ovolunlem1  25725  ioorf  25801  mbfi1fseqlem3  25945  mbfi1flim  25951  itg2seq  25970  itg2splitlem  25976  itg2split  25977  iblss  26032  itgle  26037  itgeqa  26041  ibladdlem  26047  itgaddlem1  26050  iblabslem  26055  iblabs  26056  iblabsr  26057  iblmulc2  26058  itgmulc2lem1  26059  bddmulibl  26066  bddiblnc  26069  itggt0  26071  itgcn  26072  ellimc2  26104  limccnp  26118  limccnp2  26119  dvcobr  26173  lhop1  26241  elplyd  26427  coeeq2  26468  dvply1  26514  aalioulem3  26570  dvtaylp  26606  dvradcnv  26657  psercnlem1  26661  logcnlem2  26880  logcnlem3  26881  logcnlem4  26882  logtayllem  26896  logtayl  26897  cxpcl  26911  recxpcl  26912  leibpilem2  27178  leibpi  27179  rlimcnp2  27203  efrlim  27206  igamf  27287  igamcl  27288  pclogsum  27451  dchrelbasd  27475  lgsfcl2  27539  lgscllem  27540  lgsval2lem  27543  lgsne0  27571  2sqnn0  27674  dchrvmasumiflem2  27738  dchrisum0flblem1  27744  pntrlog2bndlem4  27816  pntrlog2bndlem5  27817  pntlemj  27839  padicabv  27866  crctcshwlkn0  30289  ccatws1f1o  33393  sgnsval  33601  elrgspnlem2  33683  elrgspnlem3  33684  elrgspnlem4  33685  gsummoncoe1fzo  34007  selvascl  34027  fldextrspunlsp  34184  extdgfialglem2  34203  xrge0iifcnv  34443  xrge0iifhom  34447  pnfneige0  34461  esumpinfval  34583  sigaclfu2  34631  ballotlemsv  35021  ballotlemsdom  35023  signswmnd  35065  signsvvf  35087  signsvfn  35090  mrsubcv  36089  mrsubff  36091  mrsubrn  36092  mrsubccat  36097  unblimceq0lem  37203  ptrecube  38369  poimirlem24  38393  itg2addnclem2  38421  itg2gt0cn  38424  ibladdnclem  38425  itgaddnclem1  38427  iblabsnclem  38432  iblabsnc  38433  iblmulc2nc  38434  itgmulc2nclem1  38435  itggt0cn  38439  ftc1anclem5  38446  ftc1anclem6  38447  ftc1anclem7  38448  ftc1anclem8  38449  ftc1anc  38450  areacirc  38462  cdleme27cl  41239  dffltz  43480  cantnfub  44162  climsuse  46438  lptioo1  46462  icccncfext  46715  cncfiooicclem1  46721  iblsplit  46794  dirkerval2  46922  dirkerre  46923  fourierdlem9  46944  fourierdlem17  46952  fourierdlem43  46978  etransclem3  47065  etransclem7  47069  etransclem10  47072  etransclem21  47083  lincext1  49384