Theorem ifclda 4520

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ifcif 4484

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4485

This theorem is referenced by:  unxpdomlem3  9175  updjudhf  9860  acndom  9980  iunfictbso  10043  dfac12lem2  10074  ttukeylem6  10443  canthp1lem2  10582  xaddf  13160  xmulf  13208  ccatcl  14515  swrdcl  14586  ccatco  14777  lo1bdd2  15466  o1lo1  15479  sadadd2lem2  16396  sadcaddlem  16403  sadadd2lem  16405  sadadd3  16407  lcmfval  16567  iserodd  16782  prmreclem2  16864  prmreclem4  16866  prmreclem6  16868  prmrec  16869  vdwlem6  16933  mreexexd  17585  smndex2hbas  18819  symgextf  19323  pmtrf  19361  odfval  19438  cyggex2  19803  dprdfid  19925  dmdprdsplitlem  19945  sdrgacs  20686  cygznlem1  21452  cygznlem2a  21453  cygznlem3  21455  cygth  21457  fvmptnn04if  22712  chfacfisf  22717  chfacfisfcpmat  22718  ptpjpre2  23443  ptopn2  23447  ptpjopn  23475  iccpnfcnv  24818  xrhmeo  24820  cmetcaulem  25164  ovolunlem1a  25373  ovolunlem1  25374  ioorf  25450  mbfi1fseqlem3  25594  mbfi1flim  25600  itg2seq  25619  itg2splitlem  25625  itg2split  25626  iblss  25682  itgle  25687  itgeqa  25691  ibladdlem  25697  itgaddlem1  25700  iblabslem  25705  iblabs  25706  iblabsr  25707  iblmulc2  25708  itgmulc2lem1  25709  bddmulibl  25716  bddiblnc  25719  itggt0  25721  itgcn  25722  ellimc2  25754  limccnp  25768  limccnp2  25769  dvcobr  25825  dvcobrOLD  25826  lhop1  25895  elplyd  26083  coeeq2  26123  dvply1  26167  aalioulem3  26218  dvtaylp  26254  dvradcnv  26306  psercnlem1  26311  logcnlem2  26528  logcnlem3  26529  logcnlem4  26530  logtayllem  26544  logtayl  26545  cxpcl  26559  recxpcl  26560  leibpilem2  26827  leibpi  26828  rlimcnp2  26852  efrlim  26855  efrlimOLD  26856  igamf  26937  igamcl  26938  pclogsum  27102  dchrelbasd  27126  lgsfcl2  27190  lgscllem  27191  lgsval2lem  27194  lgsne0  27222  2sqnn0  27325  dchrvmasumiflem2  27389  dchrisum0flblem1  27395  pntrlog2bndlem4  27467  pntrlog2bndlem5  27468  pntlemj  27490  padicabv  27517  crctcshwlkn0  29724  ccatws1f1o  32846  sgnsval  33091  elrgspnlem2  33167  elrgspnlem3  33168  elrgspnlem4  33169  gsummoncoe1fzo  33536  fldextrspunlsp  33642  xrge0iifcnv  33896  xrge0iifhom  33900  pnfneige0  33914  esumpinfval  34036  sigaclfu2  34084  ballotlemsv  34474  ballotlemsdom  34476  signswmnd  34521  signsvvf  34543  signsvfn  34546  mrsubcv  35470  mrsubff  35472  mrsubrn  35473  mrsubccat  35478  unblimceq0lem  36467  ptrecube  37587  poimirlem24  37611  itg2addnclem2  37639  itg2gt0cn  37642  ibladdnclem  37643  itgaddnclem1  37645  iblabsnclem  37650  iblabsnc  37651  iblmulc2nc  37652  itgmulc2nclem1  37653  itggt0cn  37657  ftc1anclem5  37664  ftc1anclem6  37665  ftc1anclem7  37666  ftc1anclem8  37667  ftc1anc  37668  areacirc  37680  cdleme27cl  40333  selvcllem5  42543  selvvvval  42546  dffltz  42595  cantnfub  43283  climsuse  45579  lptioo1  45603  icccncfext  45858  cncfiooicclem1  45864  iblsplit  45937  dirkerval2  46065  dirkerre  46066  fourierdlem9  46087  fourierdlem17  46095  fourierdlem43  46121  etransclem3  46208  etransclem7  46212  etransclem10  46215  etransclem21  46226  lincext1  48416