Theorem ifclda 4562

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   = wceq 1539   ∈ wcel 2104  ifcif 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-if 4528

This theorem is referenced by:  unxpdomlem3  9254  updjudhf  9928  acndom  10048  iunfictbso  10111  dfac12lem2  10141  ttukeylem6  10511  canthp1lem2  10650  xaddf  13207  xmulf  13255  ccatcl  14528  swrdcl  14599  ccatco  14790  lo1bdd2  15472  o1lo1  15485  sadadd2lem2  16395  sadcaddlem  16402  sadadd2lem  16404  sadadd3  16406  lcmfval  16562  iserodd  16772  prmreclem2  16854  prmreclem4  16856  prmreclem6  16858  prmrec  16859  vdwlem6  16923  mreexexd  17596  smndex2hbas  18833  symgextf  19326  pmtrf  19364  odfval  19441  cyggex2  19806  dprdfid  19928  dmdprdsplitlem  19948  sdrgacs  20560  cygznlem1  21341  cygznlem2a  21342  cygznlem3  21344  cygth  21346  fvmptnn04if  22571  chfacfisf  22576  chfacfisfcpmat  22577  ptpjpre2  23304  ptopn2  23308  ptpjopn  23336  iccpnfcnv  24689  xrhmeo  24691  cmetcaulem  25036  ovolunlem1a  25245  ovolunlem1  25246  ioorf  25322  mbfi1fseqlem3  25467  mbfi1flim  25473  itg2seq  25492  itg2splitlem  25498  itg2split  25499  iblss  25554  itgle  25559  itgeqa  25563  ibladdlem  25569  itgaddlem1  25572  iblabslem  25577  iblabs  25578  iblabsr  25579  iblmulc2  25580  itgmulc2lem1  25581  bddmulibl  25588  bddiblnc  25591  itggt0  25593  itgcn  25594  ellimc2  25626  limccnp  25640  limccnp2  25641  dvcobr  25697  dvcobrOLD  25698  lhop1  25766  elplyd  25951  coeeq2  25991  dvply1  26033  aalioulem3  26083  dvtaylp  26118  dvradcnv  26169  psercnlem1  26173  logcnlem2  26387  logcnlem3  26388  logcnlem4  26389  logtayllem  26403  logtayl  26404  cxpcl  26418  recxpcl  26419  leibpilem2  26682  leibpi  26683  rlimcnp2  26707  efrlim  26710  igamf  26791  igamcl  26792  pclogsum  26954  dchrelbasd  26978  lgsfcl2  27042  lgscllem  27043  lgsval2lem  27046  lgsne0  27074  2sqnn0  27177  dchrvmasumiflem2  27241  dchrisum0flblem1  27247  pntrlog2bndlem4  27319  pntrlog2bndlem5  27320  pntlemj  27342  padicabv  27369  crctcshwlkn0  29342  sgnsval  32590  gsummoncoe1fzo  32943  xrge0iifcnv  33211  xrge0iifhom  33215  pnfneige0  33229  esumpinfval  33369  sigaclfu2  33417  ballotlemsv  33806  ballotlemsdom  33808  signswmnd  33866  signsvvf  33888  signsvfn  33891  mrsubcv  34799  mrsubff  34801  mrsubrn  34802  mrsubccat  34807  unblimceq0lem  35685  ptrecube  36791  poimirlem24  36815  itg2addnclem2  36843  itg2gt0cn  36846  ibladdnclem  36847  itgaddnclem1  36849  iblabsnclem  36854  iblabsnc  36855  iblmulc2nc  36856  itgmulc2nclem1  36857  itggt0cn  36861  ftc1anclem5  36868  ftc1anclem6  36869  ftc1anclem7  36870  ftc1anclem8  36871  ftc1anc  36872  areacirc  36884  cdleme27cl  39540  selvcllem5  41456  selvvvval  41459  dffltz  41678  cantnfub  42373  climsuse  44622  lptioo1  44646  icccncfext  44901  cncfiooicclem1  44907  iblsplit  44980  dirkerval2  45108  dirkerre  45109  fourierdlem9  45130  fourierdlem17  45138  fourierdlem43  45164  etransclem3  45251  etransclem7  45255  etransclem10  45258  etransclem21  45269  lincext1  47222