Theorem ifclda 4560

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ifcif 4524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-if 4525

This theorem is referenced by:  unxpdomlem3  9289  updjudhf  9972  acndom  10092  iunfictbso  10155  dfac12lem2  10186  ttukeylem6  10555  canthp1lem2  10694  xaddf  13267  xmulf  13315  ccatcl  14613  swrdcl  14684  ccatco  14875  lo1bdd2  15561  o1lo1  15574  sadadd2lem2  16488  sadcaddlem  16495  sadadd2lem  16497  sadadd3  16499  lcmfval  16659  iserodd  16874  prmreclem2  16956  prmreclem4  16958  prmreclem6  16960  prmrec  16961  vdwlem6  17025  mreexexd  17692  smndex2hbas  18930  symgextf  19436  pmtrf  19474  odfval  19551  cyggex2  19916  dprdfid  20038  dmdprdsplitlem  20058  sdrgacs  20803  cygznlem1  21586  cygznlem2a  21587  cygznlem3  21589  cygth  21591  fvmptnn04if  22856  chfacfisf  22861  chfacfisfcpmat  22862  ptpjpre2  23589  ptopn2  23593  ptpjopn  23621  iccpnfcnv  24976  xrhmeo  24978  cmetcaulem  25323  ovolunlem1a  25532  ovolunlem1  25533  ioorf  25609  mbfi1fseqlem3  25753  mbfi1flim  25759  itg2seq  25778  itg2splitlem  25784  itg2split  25785  iblss  25841  itgle  25846  itgeqa  25850  ibladdlem  25856  itgaddlem1  25859  iblabslem  25864  iblabs  25865  iblabsr  25866  iblmulc2  25867  itgmulc2lem1  25868  bddmulibl  25875  bddiblnc  25878  itggt0  25880  itgcn  25881  ellimc2  25913  limccnp  25927  limccnp2  25928  dvcobr  25984  dvcobrOLD  25985  lhop1  26054  elplyd  26242  coeeq2  26282  dvply1  26326  aalioulem3  26377  dvtaylp  26413  dvradcnv  26465  psercnlem1  26470  logcnlem2  26686  logcnlem3  26687  logcnlem4  26688  logtayllem  26702  logtayl  26703  cxpcl  26717  recxpcl  26718  leibpilem2  26985  leibpi  26986  rlimcnp2  27010  efrlim  27013  efrlimOLD  27014  igamf  27095  igamcl  27096  pclogsum  27260  dchrelbasd  27284  lgsfcl2  27348  lgscllem  27349  lgsval2lem  27352  lgsne0  27380  2sqnn0  27483  dchrvmasumiflem2  27547  dchrisum0flblem1  27553  pntrlog2bndlem4  27625  pntrlog2bndlem5  27626  pntlemj  27648  padicabv  27675  crctcshwlkn0  29842  ccatws1f1o  32937  sgnsval  33182  elrgspnlem2  33248  elrgspnlem3  33249  elrgspnlem4  33250  gsummoncoe1fzo  33619  fldextrspunlsp  33725  xrge0iifcnv  33933  xrge0iifhom  33937  pnfneige0  33951  esumpinfval  34075  sigaclfu2  34123  ballotlemsv  34513  ballotlemsdom  34515  signswmnd  34573  signsvvf  34595  signsvfn  34598  mrsubcv  35516  mrsubff  35518  mrsubrn  35519  mrsubccat  35524  unblimceq0lem  36508  ptrecube  37628  poimirlem24  37652  itg2addnclem2  37680  itg2gt0cn  37683  ibladdnclem  37684  itgaddnclem1  37686  iblabsnclem  37691  iblabsnc  37692  iblmulc2nc  37693  itgmulc2nclem1  37694  itggt0cn  37698  ftc1anclem5  37705  ftc1anclem6  37706  ftc1anclem7  37707  ftc1anclem8  37708  ftc1anc  37709  areacirc  37721  cdleme27cl  40369  selvcllem5  42597  selvvvval  42600  dffltz  42649  cantnfub  43339  climsuse  45628  lptioo1  45652  icccncfext  45907  cncfiooicclem1  45913  iblsplit  45986  dirkerval2  46114  dirkerre  46115  fourierdlem9  46136  fourierdlem17  46144  fourierdlem43  46170  etransclem3  46257  etransclem7  46261  etransclem10  46264  etransclem21  46275  lincext1  48376