Theorem ifclda 4518

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 4488	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 487	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifclda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2861	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5		iffalse 4491	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 487	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifclda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
8	6, 7	eqeltrd 2861	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
9	4, 8	pm2.61dan 825	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4483

This theorem is used by:  unxpdomlem3  9242  updjudhf  10005  acndom  10123  iunfictbso  10186  dfac12lem2  10216  ttukeylem6  10585  canthp1lem2  10731  xaddf  13347  xmulf  13395  ccatcl  14712  swrdcl  14786  ccatco  14979  lo1bdd2  15684  o1lo1  15697  sadadd2lem2  16613  sadcaddlem  16620  sadadd2lem  16622  sadadd3  16624  lcmfval  16789  iserodd  17006  prmreclem2  17088  prmreclem4  17090  prmreclem6  17092  prmrec  17093  vdwlem6  17157  mreexexd  17815  smndex2hbas  19108  symgextf  19624  pmtrf  19662  odfval  19739  cyggex2  20104  dprdfid  20226  dmdprdsplitlem  20246  sdrgacs  21051  cygznlem1  21865  cygznlem2a  21866  cygznlem3  21868  cygth  21870  selvcllem5  22441  selvvvval  22444  fvmptnn04if  23160  chfacfisf  23165  chfacfisfcpmat  23166  ptpjpre2  23892  ptopn2  23896  ptpjopn  23924  iccpnfcnv  25258  xrhmeo  25260  cmetcaulem  25602  ovolunlem1a  25810  ovolunlem1  25811  ioorf  25887  mbfi1fseqlem3  26031  mbfi1flim  26037  itg2seq  26056  itg2splitlem  26062  itg2split  26063  iblss  26118  itgle  26123  itgeqa  26127  ibladdlem  26133  itgaddlem1  26136  iblabslem  26141  iblabs  26142  iblabsr  26143  iblmulc2  26144  itgmulc2lem1  26145  bddmulibl  26152  bddiblnc  26155  itggt0  26157  itgcn  26158  ellimc2  26190  limccnp  26204  limccnp2  26205  dvcobr  26259  lhop1  26327  elplyd  26513  coeeq2  26554  dvply1  26598  aalioulem3  26654  dvtaylp  26690  dvradcnv  26741  psercnlem1  26745  logcnlem2  26964  logcnlem3  26965  logcnlem4  26966  logtayllem  26980  logtayl  26981  cxpcl  26995  recxpcl  26996  leibpilem2  27262  leibpi  27263  rlimcnp2  27287  efrlim  27290  igamf  27371  igamcl  27372  pclogsum  27535  dchrelbasd  27559  lgsfcl2  27623  lgscllem  27624  lgsval2lem  27627  lgsne0  27655  2sqnn0  27758  dchrvmasumiflem2  27822  dchrisum0flblem1  27828  pntrlog2bndlem4  27900  pntrlog2bndlem5  27901  pntlemj  27923  padicabv  27950  crctcshwlkn0  30403  ccatws1f1o  33507  sgnsval  33715  elrgspnlem2  33797  elrgspnlem3  33798  elrgspnlem4  33799  gsummoncoe1fzo  34122  selvascl  34142  fldextrspunlsp  34299  extdgfialglem2  34318  xrge0iifcnv  34558  xrge0iifhom  34562  pnfneige0  34576  esumpinfval  34698  sigaclfu2  34746  ballotlemsv  35135  ballotlemsdom  35137  signswmnd  35179  signsvvf  35201  signsvfn  35204  mrsubcv  36254  mrsubff  36256  mrsubrn  36257  mrsubccat  36262  unblimceq0lem  37352  ptrecube  38518  poimirlem24  38542  itg2addnclem2  38570  itg2gt0cn  38573  ibladdnclem  38574  itgaddnclem1  38576  iblabsnclem  38581  iblabsnc  38582  iblmulc2nc  38583  itgmulc2nclem1  38584  itggt0cn  38588  ftc1anclem5  38595  ftc1anclem6  38596  ftc1anclem7  38597  ftc1anclem8  38598  ftc1anc  38599  areacirc  38611  cdleme27cl  41403  dffltz  43650  cantnfub  44307  climsuse  46589  lptioo1  46613  icccncfext  46866  cncfiooicclem1  46872  iblsplit  46945  dirkerval2  47073  dirkerre  47074  fourierdlem9  47095  fourierdlem17  47103  fourierdlem43  47129  etransclem3  47216  etransclem7  47220  etransclem10  47223  etransclem21  47234  lincext1  49535