Theorem ifclda 4521

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 4491	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 487	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifclda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2864	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5		iffalse 4494	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 487	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifclda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
8	6, 7	eqeltrd 2864	. 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 2147  ifcif 4485

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-if 4486

This theorem is used by:  unxpdomlem3  9285  updjudhf  10047  acndom  10167  iunfictbso  10230  dfac12lem2  10260  ttukeylem6  10629  canthp1lem2  10775  xaddf  13392  xmulf  13440  ccatcl  14758  swrdcl  14833  ccatco  15026  lo1bdd2  15732  o1lo1  15745  sadadd2lem2  16661  sadcaddlem  16668  sadadd2lem  16670  sadadd3  16672  lcmfval  16837  iserodd  17054  prmreclem2  17136  prmreclem4  17138  prmreclem6  17140  prmrec  17141  vdwlem6  17205  mreexexd  17863  smndex2hbas  19156  symgextf  19673  pmtrf  19711  odfval  19788  cyggex2  20153  dprdfid  20275  dmdprdsplitlem  20295  sdrgacs  21100  cygznlem1  21916  cygznlem2a  21917  cygznlem3  21919  cygth  21921  selvcllem5  22492  selvvvval  22495  fvmptnn04if  23211  chfacfisf  23216  chfacfisfcpmat  23217  ptpjpre2  23943  ptopn2  23947  ptpjopn  23975  iccpnfcnv  25309  xrhmeo  25311  cmetcaulem  25653  ovolunlem1a  25861  ovolunlem1  25862  ioorf  25938  mbfi1fseqlem3  26082  mbfi1flim  26088  itg2seq  26107  itg2splitlem  26113  itg2split  26114  iblss  26169  itgle  26174  itgeqa  26178  ibladdlem  26184  itgaddlem1  26187  iblabslem  26192  iblabs  26193  iblabsr  26194  iblmulc2  26195  itgmulc2lem1  26196  bddmulibl  26203  bddiblnc  26206  itggt0  26208  itgcn  26209  ellimc2  26241  limccnp  26255  limccnp2  26256  dvcobr  26310  lhop1  26378  elplyd  26564  coeeq2  26605  dvply1  26649  aalioulem3  26707  dvtaylp  26743  dvradcnv  26794  psercnlem1  26798  logcnlem2  27017  logcnlem3  27018  logcnlem4  27019  logtayllem  27033  logtayl  27034  cxpcl  27048  recxpcl  27049  leibpilem2  27315  leibpi  27316  rlimcnp2  27340  efrlim  27343  igamf  27424  igamcl  27425  pclogsum  27588  dchrelbasd  27612  lgsfcl2  27676  lgscllem  27677  lgsval2lem  27680  lgsne0  27708  2sqnn0  27811  dchrvmasumiflem2  27875  dchrisum0flblem1  27881  pntrlog2bndlem4  27953  pntrlog2bndlem5  27954  pntlemj  27976  padicabv  28003  crctcshwlkn0  30456  ccatws1f1o  33600  sgnsval  33811  elrgspnlem2  33893  elrgspnlem3  33894  elrgspnlem4  33895  gsummoncoe1fzo  34225  selvascl  34253  fldextrspunlsp  34410  extdgfialglem2  34429  xrge0iifcnv  34669  xrge0iifhom  34673  pnfneige0  34687  esumpinfval  34809  sigaclfu2  34857  ballotlemsv  35246  ballotlemsdom  35248  signswmnd  35290  signsvvf  35312  signsvfn  35315  mrsubcv  36476  mrsubff  36478  mrsubrn  36479  mrsubccat  36484  unblimceq0lem  37580  ptrecube  38799  poimirlem24  38823  itg2addnclem2  38851  itg2gt0cn  38854  ibladdnclem  38855  itgaddnclem1  38857  iblabsnclem  38862  iblabsnc  38863  iblmulc2nc  38864  itgmulc2nclem1  38865  itggt0cn  38869  ftc1anclem5  38876  ftc1anclem6  38877  ftc1anclem7  38878  ftc1anclem8  38879  ftc1anc  38880  areacirc  38892  cdleme27cl  41682  dffltz  43930  cantnfub  44578  climsuse  46887  lptioo1  46911  icccncfext  47164  cncfiooicclem1  47170  iblsplit  47243  dirkerval2  47371  dirkerre  47372  fourierdlem9  47393  fourierdlem17  47401  fourierdlem43  47427  etransclem3  47514  etransclem7  47518  etransclem10  47521  etransclem21  47532  lincext1  49891