Theorem ifclda 4503

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 4473	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifclda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2837	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5		iffalse 4476	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 481	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifclda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
8	6, 7	eqeltrd 2837	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
9	4, 8	pm2.61dan 813	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4468

This theorem is referenced by:  unxpdomlem3  9161  updjudhf  9846  acndom  9964  iunfictbso  10027  dfac12lem2  10058  ttukeylem6  10427  canthp1lem2  10567  xaddf  13167  xmulf  13215  ccatcl  14527  swrdcl  14599  ccatco  14788  lo1bdd2  15477  o1lo1  15490  sadadd2lem2  16410  sadcaddlem  16417  sadadd2lem  16419  sadadd3  16421  lcmfval  16581  iserodd  16797  prmreclem2  16879  prmreclem4  16881  prmreclem6  16883  prmrec  16884  vdwlem6  16948  mreexexd  17605  smndex2hbas  18878  symgextf  19383  pmtrf  19421  odfval  19498  cyggex2  19863  dprdfid  19985  dmdprdsplitlem  20005  sdrgacs  20769  cygznlem1  21556  cygznlem2a  21557  cygznlem3  21559  cygth  21561  fvmptnn04if  22824  chfacfisf  22829  chfacfisfcpmat  22830  ptpjpre2  23555  ptopn2  23559  ptpjopn  23587  iccpnfcnv  24921  xrhmeo  24923  cmetcaulem  25265  ovolunlem1a  25473  ovolunlem1  25474  ioorf  25550  mbfi1fseqlem3  25694  mbfi1flim  25700  itg2seq  25719  itg2splitlem  25725  itg2split  25726  iblss  25782  itgle  25787  itgeqa  25791  ibladdlem  25797  itgaddlem1  25800  iblabslem  25805  iblabs  25806  iblabsr  25807  iblmulc2  25808  itgmulc2lem1  25809  bddmulibl  25816  bddiblnc  25819  itggt0  25821  itgcn  25822  ellimc2  25854  limccnp  25868  limccnp2  25869  dvcobr  25923  lhop1  25991  elplyd  26177  coeeq2  26217  dvply1  26260  aalioulem3  26311  dvtaylp  26347  dvradcnv  26399  psercnlem1  26403  logcnlem2  26620  logcnlem3  26621  logcnlem4  26622  logtayllem  26636  logtayl  26637  cxpcl  26651  recxpcl  26652  leibpilem2  26918  leibpi  26919  rlimcnp2  26943  efrlim  26946  efrlimOLD  26947  igamf  27028  igamcl  27029  pclogsum  27192  dchrelbasd  27216  lgsfcl2  27280  lgscllem  27281  lgsval2lem  27284  lgsne0  27312  2sqnn0  27415  dchrvmasumiflem2  27479  dchrisum0flblem1  27485  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  pntlemj  27580  padicabv  27607  crctcshwlkn0  29904  ccatws1f1o  33026  sgnsval  33237  elrgspnlem2  33319  elrgspnlem3  33320  elrgspnlem4  33321  gsummoncoe1fzo  33672  fldextrspunlsp  33834  extdgfialglem2  33853  xrge0iifcnv  34093  xrge0iifhom  34097  pnfneige0  34111  esumpinfval  34233  sigaclfu2  34281  ballotlemsv  34670  ballotlemsdom  34672  signswmnd  34717  signsvvf  34739  signsvfn  34742  mrsubcv  35708  mrsubff  35710  mrsubrn  35711  mrsubccat  35716  unblimceq0lem  36782  ptrecube  37955  poimirlem24  37979  itg2addnclem2  38007  itg2gt0cn  38010  ibladdnclem  38011  itgaddnclem1  38013  iblabsnclem  38018  iblabsnc  38019  iblmulc2nc  38020  itgmulc2nclem1  38021  itggt0cn  38025  ftc1anclem5  38032  ftc1anclem6  38033  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  areacirc  38048  cdleme27cl  40826  selvcllem5  43029  selvvvval  43032  dffltz  43081  cantnfub  43767  climsuse  46056  lptioo1  46080  icccncfext  46333  cncfiooicclem1  46339  iblsplit  46412  dirkerval2  46540  dirkerre  46541  fourierdlem9  46562  fourierdlem17  46570  fourierdlem43  46596  etransclem3  46683  etransclem7  46687  etransclem10  46690  etransclem21  46701  lincext1  48942