Theorem ifclda 4517

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ifcif 4481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4482

This theorem is referenced by:  unxpdomlem3  9170  updjudhf  9855  acndom  9973  iunfictbso  10036  dfac12lem2  10067  ttukeylem6  10436  canthp1lem2  10576  xaddf  13151  xmulf  13199  ccatcl  14509  swrdcl  14581  ccatco  14770  lo1bdd2  15459  o1lo1  15472  sadadd2lem2  16389  sadcaddlem  16396  sadadd2lem  16398  sadadd3  16400  lcmfval  16560  iserodd  16775  prmreclem2  16857  prmreclem4  16859  prmreclem6  16861  prmrec  16862  vdwlem6  16926  mreexexd  17583  smndex2hbas  18853  symgextf  19358  pmtrf  19396  odfval  19473  cyggex2  19838  dprdfid  19960  dmdprdsplitlem  19980  sdrgacs  20746  cygznlem1  21533  cygznlem2a  21534  cygznlem3  21536  cygth  21538  fvmptnn04if  22805  chfacfisf  22810  chfacfisfcpmat  22811  ptpjpre2  23536  ptopn2  23540  ptpjopn  23568  iccpnfcnv  24910  xrhmeo  24912  cmetcaulem  25256  ovolunlem1a  25465  ovolunlem1  25466  ioorf  25542  mbfi1fseqlem3  25686  mbfi1flim  25692  itg2seq  25711  itg2splitlem  25717  itg2split  25718  iblss  25774  itgle  25779  itgeqa  25783  ibladdlem  25789  itgaddlem1  25792  iblabslem  25797  iblabs  25798  iblabsr  25799  iblmulc2  25800  itgmulc2lem1  25801  bddmulibl  25808  bddiblnc  25811  itggt0  25813  itgcn  25814  ellimc2  25846  limccnp  25860  limccnp2  25861  dvcobr  25917  dvcobrOLD  25918  lhop1  25987  elplyd  26175  coeeq2  26215  dvply1  26259  aalioulem3  26310  dvtaylp  26346  dvradcnv  26398  psercnlem1  26403  logcnlem2  26620  logcnlem3  26621  logcnlem4  26622  logtayllem  26636  logtayl  26637  cxpcl  26651  recxpcl  26652  leibpilem2  26919  leibpi  26920  rlimcnp2  26944  efrlim  26947  efrlimOLD  26948  igamf  27029  igamcl  27030  pclogsum  27194  dchrelbasd  27218  lgsfcl2  27282  lgscllem  27283  lgsval2lem  27286  lgsne0  27314  2sqnn0  27417  dchrvmasumiflem2  27481  dchrisum0flblem1  27487  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntlemj  27582  padicabv  27609  crctcshwlkn0  29906  ccatws1f1o  33043  sgnsval  33254  elrgspnlem2  33336  elrgspnlem3  33337  elrgspnlem4  33338  gsummoncoe1fzo  33689  fldextrspunlsp  33851  extdgfialglem2  33870  xrge0iifcnv  34110  xrge0iifhom  34114  pnfneige0  34128  esumpinfval  34250  sigaclfu2  34298  ballotlemsv  34687  ballotlemsdom  34689  signswmnd  34734  signsvvf  34756  signsvfn  34759  mrsubcv  35723  mrsubff  35725  mrsubrn  35726  mrsubccat  35731  unblimceq0lem  36725  ptrecube  37868  poimirlem24  37892  itg2addnclem2  37920  itg2gt0cn  37923  ibladdnclem  37924  itgaddnclem1  37926  iblabsnclem  37931  iblabsnc  37932  iblmulc2nc  37933  itgmulc2nclem1  37934  itggt0cn  37938  ftc1anclem5  37945  ftc1anclem6  37946  ftc1anclem7  37947  ftc1anclem8  37948  ftc1anc  37949  areacirc  37961  cdleme27cl  40739  selvcllem5  42937  selvvvval  42940  dffltz  42989  cantnfub  43675  climsuse  45965  lptioo1  45989  icccncfext  46242  cncfiooicclem1  46248  iblsplit  46321  dirkerval2  46449  dirkerre  46450  fourierdlem9  46471  fourierdlem17  46479  fourierdlem43  46505  etransclem3  46592  etransclem7  46596  etransclem10  46599  etransclem21  46610  lincext1  48811