Theorem ifclda 4525

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 4495	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 486	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifclda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2869	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5		iffalse 4498	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 486	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifclda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
8	6, 7	eqeltrd 2869	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
9	4, 8	pm2.61dan 824	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ifcif 4489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-if 4490

This theorem is referenced by:  unxpdomlem3  9214  updjudhf  9913  acndom  10031  iunfictbso  10094  dfac12lem2  10124  ttukeylem6  10494  canthp1lem2  10634  xaddf  13246  xmulf  13294  ccatcl  14607  swrdcl  14679  ccatco  14868  lo1bdd2  15571  o1lo1  15584  sadadd2lem2  16504  sadcaddlem  16511  sadadd2lem  16513  sadadd3  16515  lcmfval  16675  iserodd  16891  prmreclem2  16973  prmreclem4  16975  prmreclem6  16977  prmrec  16978  vdwlem6  17042  mreexexd  17700  smndex2hbas  18974  symgextf  19483  pmtrf  19521  odfval  19598  cyggex2  19963  dprdfid  20085  dmdprdsplitlem  20105  sdrgacs  20878  cygznlem1  21681  cygznlem2a  21682  cygznlem3  21684  cygth  21686  selvcllem5  22255  selvvvval  22258  fvmptnn04if  22971  chfacfisf  22976  chfacfisfcpmat  22977  ptpjpre2  23702  ptopn2  23706  ptpjopn  23734  iccpnfcnv  25068  xrhmeo  25070  cmetcaulem  25412  ovolunlem1a  25620  ovolunlem1  25621  ioorf  25697  mbfi1fseqlem3  25841  mbfi1flim  25847  itg2seq  25866  itg2splitlem  25872  itg2split  25873  iblss  25929  itgle  25934  itgeqa  25938  ibladdlem  25944  itgaddlem1  25947  iblabslem  25952  iblabs  25953  iblabsr  25954  iblmulc2  25955  itgmulc2lem1  25956  bddmulibl  25963  bddiblnc  25966  itggt0  25968  itgcn  25969  ellimc2  26001  limccnp  26015  limccnp2  26016  dvcobr  26070  lhop1  26138  elplyd  26324  coeeq2  26364  dvply1  26410  aalioulem3  26460  dvtaylp  26495  dvradcnv  26546  psercnlem1  26550  logcnlem2  26770  logcnlem3  26771  logcnlem4  26772  logtayllem  26786  logtayl  26787  cxpcl  26801  recxpcl  26802  leibpilem2  27068  leibpi  27069  rlimcnp2  27093  efrlim  27096  igamf  27177  igamcl  27178  pclogsum  27341  dchrelbasd  27365  lgsfcl2  27429  lgscllem  27430  lgsval2lem  27433  lgsne0  27461  2sqnn0  27564  dchrvmasumiflem2  27628  dchrisum0flblem1  27634  pntrlog2bndlem4  27706  pntrlog2bndlem5  27707  pntlemj  27729  padicabv  27756  crctcshwlkn0  30107  ccatws1f1o  33208  sgnsval  33418  elrgspnlem2  33500  elrgspnlem3  33501  elrgspnlem4  33502  gsummoncoe1fzo  33828  selvascl  33848  fldextrspunlsp  34005  extdgfialglem2  34024  xrge0iifcnv  34264  xrge0iifhom  34268  pnfneige0  34282  esumpinfval  34404  sigaclfu2  34452  ballotlemsv  34841  ballotlemsdom  34843  signswmnd  34885  signsvvf  34907  signsvfn  34910  mrsubcv  35897  mrsubff  35899  mrsubrn  35900  mrsubccat  35905  unblimceq0lem  36980  ptrecube  38154  poimirlem24  38178  itg2addnclem2  38206  itg2gt0cn  38209  ibladdnclem  38210  itgaddnclem1  38212  iblabsnclem  38217  iblabsnc  38218  iblmulc2nc  38219  itgmulc2nclem1  38220  itggt0cn  38224  ftc1anclem5  38231  ftc1anclem6  38232  ftc1anclem7  38233  ftc1anclem8  38234  ftc1anc  38235  areacirc  38247  cdleme27cl  41025  dffltz  43251  cantnfub  43933  climsuse  46209  lptioo1  46233  icccncfext  46486  cncfiooicclem1  46492  iblsplit  46565  dirkerval2  46693  dirkerre  46694  fourierdlem9  46715  fourierdlem17  46723  fourierdlem43  46749  etransclem3  46836  etransclem7  46840  etransclem10  46843  etransclem21  46854  lincext1  49112