Theorem ifclda 4502

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4467

This theorem is referenced by:  unxpdomlem3  9168  updjudhf  9855  acndom  9973  iunfictbso  10036  dfac12lem2  10067  ttukeylem6  10436  canthp1lem2  10576  xaddf  13176  xmulf  13224  ccatcl  14536  swrdcl  14608  ccatco  14797  lo1bdd2  15486  o1lo1  15499  sadadd2lem2  16419  sadcaddlem  16426  sadadd2lem  16428  sadadd3  16430  lcmfval  16590  iserodd  16806  prmreclem2  16888  prmreclem4  16890  prmreclem6  16892  prmrec  16893  vdwlem6  16957  mreexexd  17614  smndex2hbas  18887  symgextf  19392  pmtrf  19430  odfval  19507  cyggex2  19872  dprdfid  19994  dmdprdsplitlem  20014  sdrgacs  20778  cygznlem1  21546  cygznlem2a  21547  cygznlem3  21549  cygth  21551  fvmptnn04if  22814  chfacfisf  22819  chfacfisfcpmat  22820  ptpjpre2  23545  ptopn2  23549  ptpjopn  23577  iccpnfcnv  24911  xrhmeo  24913  cmetcaulem  25255  ovolunlem1a  25463  ovolunlem1  25464  ioorf  25540  mbfi1fseqlem3  25684  mbfi1flim  25690  itg2seq  25709  itg2splitlem  25715  itg2split  25716  iblss  25772  itgle  25777  itgeqa  25781  ibladdlem  25787  itgaddlem1  25790  iblabslem  25795  iblabs  25796  iblabsr  25797  iblmulc2  25798  itgmulc2lem1  25799  bddmulibl  25806  bddiblnc  25809  itggt0  25811  itgcn  25812  ellimc2  25844  limccnp  25858  limccnp2  25859  dvcobr  25913  lhop1  25981  elplyd  26167  coeeq2  26207  dvply1  26250  aalioulem3  26300  dvtaylp  26335  dvradcnv  26386  psercnlem1  26390  logcnlem2  26607  logcnlem3  26608  logcnlem4  26609  logtayllem  26623  logtayl  26624  cxpcl  26638  recxpcl  26639  leibpilem2  26905  leibpi  26906  rlimcnp2  26930  efrlim  26933  igamf  27014  igamcl  27015  pclogsum  27178  dchrelbasd  27202  lgsfcl2  27266  lgscllem  27267  lgsval2lem  27270  lgsne0  27298  2sqnn0  27401  dchrvmasumiflem2  27465  dchrisum0flblem1  27471  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntlemj  27566  padicabv  27593  crctcshwlkn0  29889  ccatws1f1o  33011  sgnsval  33222  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnlem4  33306  gsummoncoe1fzo  33657  fldextrspunlsp  33818  extdgfialglem2  33837  xrge0iifcnv  34077  xrge0iifhom  34081  pnfneige0  34095  esumpinfval  34217  sigaclfu2  34265  ballotlemsv  34654  ballotlemsdom  34656  signswmnd  34701  signsvvf  34723  signsvfn  34726  mrsubcv  35692  mrsubff  35694  mrsubrn  35695  mrsubccat  35700  unblimceq0lem  36766  ptrecube  37941  poimirlem24  37965  itg2addnclem2  37993  itg2gt0cn  37996  ibladdnclem  37997  itgaddnclem1  37999  iblabsnclem  38004  iblabsnc  38005  iblmulc2nc  38006  itgmulc2nclem1  38007  itggt0cn  38011  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  areacirc  38034  cdleme27cl  40812  selvcllem5  43015  selvvvval  43018  dffltz  43067  cantnfub  43749  climsuse  46038  lptioo1  46062  icccncfext  46315  cncfiooicclem1  46321  iblsplit  46394  dirkerval2  46522  dirkerre  46523  fourierdlem9  46544  fourierdlem17  46552  fourierdlem43  46578  etransclem3  46665  etransclem7  46669  etransclem10  46672  etransclem21  46683  lincext1  48930