Theorem ifclda 4491

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-if 4457

This theorem is referenced by:  unxpdomlem3  8958  updjudhf  9620  acndom  9738  iunfictbso  9801  dfac12lem2  9831  ttukeylem6  10201  canthp1lem2  10340  xaddf  12887  xmulf  12935  ccatcl  14205  swrdcl  14286  ccatco  14476  lo1bdd2  15161  o1lo1  15174  sadadd2lem2  16085  sadcaddlem  16092  sadadd2lem  16094  sadadd3  16096  lcmfval  16254  iserodd  16464  prmreclem2  16546  prmreclem4  16548  prmreclem6  16550  prmrec  16551  vdwlem6  16615  mreexexd  17274  smndex2hbas  18470  symgextf  18940  pmtrf  18978  odfval  19055  cyggex2  19413  dprdfid  19535  dmdprdsplitlem  19555  sdrgacs  19984  cygznlem1  20686  cygznlem2a  20687  cygznlem3  20689  cygth  20691  fvmptnn04if  21906  chfacfisf  21911  chfacfisfcpmat  21912  ptpjpre2  22639  ptopn2  22643  ptpjopn  22671  iccpnfcnv  24013  xrhmeo  24015  cmetcaulem  24357  ovolunlem1a  24565  ovolunlem1  24566  ioorf  24642  mbfi1fseqlem3  24787  mbfi1flim  24793  itg2seq  24812  itg2splitlem  24818  itg2split  24819  iblss  24874  itgle  24879  itgeqa  24883  ibladdlem  24889  itgaddlem1  24892  iblabslem  24897  iblabs  24898  iblabsr  24899  iblmulc2  24900  itgmulc2lem1  24901  bddmulibl  24908  bddiblnc  24911  itggt0  24913  itgcn  24914  ellimc2  24946  limccnp  24960  limccnp2  24961  dvcobr  25015  lhop1  25083  elplyd  25268  coeeq2  25308  dvply1  25349  aalioulem3  25399  dvtaylp  25434  dvradcnv  25485  psercnlem1  25489  logcnlem2  25703  logcnlem3  25704  logcnlem4  25705  logtayllem  25719  logtayl  25720  cxpcl  25734  recxpcl  25735  leibpilem2  25996  leibpi  25997  rlimcnp2  26021  efrlim  26024  igamf  26105  igamcl  26106  pclogsum  26268  dchrelbasd  26292  lgsfcl2  26356  lgscllem  26357  lgsval2lem  26360  lgsne0  26388  2sqnn0  26491  dchrvmasumiflem2  26555  dchrisum0flblem1  26561  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntlemj  26656  padicabv  26683  crctcshwlkn0  28087  sgnsval  31330  xrge0iifcnv  31785  xrge0iifhom  31789  pnfneige0  31803  esumpinfval  31941  sigaclfu2  31989  ballotlemsv  32376  ballotlemsdom  32378  signswmnd  32436  signsvvf  32458  signsvfn  32461  mrsubcv  33372  mrsubff  33374  mrsubrn  33375  mrsubccat  33380  unblimceq0lem  34613  ptrecube  35704  poimirlem24  35728  itg2addnclem2  35756  itg2gt0cn  35759  ibladdnclem  35760  itgaddnclem1  35762  iblabsnclem  35767  iblabsnc  35768  iblmulc2nc  35769  itgmulc2nclem1  35770  itggt0cn  35774  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  areacirc  35797  cdleme27cl  38307  selvval2lem5  40155  dffltz  40387  climsuse  43039  lptioo1  43063  icccncfext  43318  cncfiooicclem1  43324  iblsplit  43397  dirkerval2  43525  dirkerre  43526  fourierdlem9  43547  fourierdlem17  43555  fourierdlem43  43581  etransclem3  43668  etransclem7  43672  etransclem10  43675  etransclem21  43686  lincext1  45683