Theorem ifclda 4514

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ifcif 4478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4479

This theorem is referenced by:  unxpdomlem3  9157  updjudhf  9846  acndom  9964  iunfictbso  10027  dfac12lem2  10058  ttukeylem6  10427  canthp1lem2  10566  xaddf  13145  xmulf  13193  ccatcl  14500  swrdcl  14571  ccatco  14761  lo1bdd2  15450  o1lo1  15463  sadadd2lem2  16380  sadcaddlem  16387  sadadd2lem  16389  sadadd3  16391  lcmfval  16551  iserodd  16766  prmreclem2  16848  prmreclem4  16850  prmreclem6  16852  prmrec  16853  vdwlem6  16917  mreexexd  17573  smndex2hbas  18809  symgextf  19315  pmtrf  19353  odfval  19430  cyggex2  19795  dprdfid  19917  dmdprdsplitlem  19937  sdrgacs  20705  cygznlem1  21492  cygznlem2a  21493  cygznlem3  21495  cygth  21497  fvmptnn04if  22753  chfacfisf  22758  chfacfisfcpmat  22759  ptpjpre2  23484  ptopn2  23488  ptpjopn  23516  iccpnfcnv  24859  xrhmeo  24861  cmetcaulem  25205  ovolunlem1a  25414  ovolunlem1  25415  ioorf  25491  mbfi1fseqlem3  25635  mbfi1flim  25641  itg2seq  25660  itg2splitlem  25666  itg2split  25667  iblss  25723  itgle  25728  itgeqa  25732  ibladdlem  25738  itgaddlem1  25741  iblabslem  25746  iblabs  25747  iblabsr  25748  iblmulc2  25749  itgmulc2lem1  25750  bddmulibl  25757  bddiblnc  25760  itggt0  25762  itgcn  25763  ellimc2  25795  limccnp  25809  limccnp2  25810  dvcobr  25866  dvcobrOLD  25867  lhop1  25936  elplyd  26124  coeeq2  26164  dvply1  26208  aalioulem3  26259  dvtaylp  26295  dvradcnv  26347  psercnlem1  26352  logcnlem2  26569  logcnlem3  26570  logcnlem4  26571  logtayllem  26585  logtayl  26586  cxpcl  26600  recxpcl  26601  leibpilem2  26868  leibpi  26869  rlimcnp2  26893  efrlim  26896  efrlimOLD  26897  igamf  26978  igamcl  26979  pclogsum  27143  dchrelbasd  27167  lgsfcl2  27231  lgscllem  27232  lgsval2lem  27235  lgsne0  27263  2sqnn0  27366  dchrvmasumiflem2  27430  dchrisum0flblem1  27436  pntrlog2bndlem4  27508  pntrlog2bndlem5  27509  pntlemj  27531  padicabv  27558  crctcshwlkn0  29785  ccatws1f1o  32912  sgnsval  33122  elrgspnlem2  33202  elrgspnlem3  33203  elrgspnlem4  33204  gsummoncoe1fzo  33549  fldextrspunlsp  33660  extdgfialglem2  33679  xrge0iifcnv  33919  xrge0iifhom  33923  pnfneige0  33937  esumpinfval  34059  sigaclfu2  34107  ballotlemsv  34497  ballotlemsdom  34499  signswmnd  34544  signsvvf  34566  signsvfn  34569  mrsubcv  35502  mrsubff  35504  mrsubrn  35505  mrsubccat  35510  unblimceq0lem  36499  ptrecube  37619  poimirlem24  37643  itg2addnclem2  37671  itg2gt0cn  37674  ibladdnclem  37675  itgaddnclem1  37677  iblabsnclem  37682  iblabsnc  37683  iblmulc2nc  37684  itgmulc2nclem1  37685  itggt0cn  37689  ftc1anclem5  37696  ftc1anclem6  37697  ftc1anclem7  37698  ftc1anclem8  37699  ftc1anc  37700  areacirc  37712  cdleme27cl  40365  selvcllem5  42575  selvvvval  42578  dffltz  42627  cantnfub  43314  climsuse  45609  lptioo1  45633  icccncfext  45888  cncfiooicclem1  45894  iblsplit  45967  dirkerval2  46095  dirkerre  46096  fourierdlem9  46117  fourierdlem17  46125  fourierdlem43  46151  etransclem3  46238  etransclem7  46242  etransclem10  46245  etransclem21  46256  lincext1  48459