Theorem ifclda 4524

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 4494	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 486	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifclda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2863	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5		iffalse 4497	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 486	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifclda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
8	6, 7	eqeltrd 2863	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
9	4, 8	pm2.61dan 824	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ifcif 4488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-if 4489

This theorem is referenced by:  unxpdomlem3  9219  updjudhf  9918  acndom  10036  iunfictbso  10099  dfac12lem2  10129  ttukeylem6  10499  canthp1lem2  10639  xaddf  13251  xmulf  13299  ccatcl  14613  swrdcl  14685  ccatco  14874  lo1bdd2  15577  o1lo1  15590  sadadd2lem2  16509  sadcaddlem  16516  sadadd2lem  16518  sadadd3  16520  lcmfval  16680  iserodd  16896  prmreclem2  16978  prmreclem4  16980  prmreclem6  16982  prmrec  16983  vdwlem6  17047  mreexexd  17705  smndex2hbas  18979  symgextf  19488  pmtrf  19526  odfval  19603  cyggex2  19968  dprdfid  20090  dmdprdsplitlem  20110  sdrgacs  20885  cygznlem1  21697  cygznlem2a  21698  cygznlem3  21700  cygth  21702  selvcllem5  22271  selvvvval  22274  fvmptnn04if  22987  chfacfisf  22992  chfacfisfcpmat  22993  ptpjpre2  23718  ptopn2  23722  ptpjopn  23750  iccpnfcnv  25084  xrhmeo  25086  cmetcaulem  25428  ovolunlem1a  25636  ovolunlem1  25637  ioorf  25713  mbfi1fseqlem3  25857  mbfi1flim  25863  itg2seq  25882  itg2splitlem  25888  itg2split  25889  iblss  25945  itgle  25950  itgeqa  25954  ibladdlem  25960  itgaddlem1  25963  iblabslem  25968  iblabs  25969  iblabsr  25970  iblmulc2  25971  itgmulc2lem1  25972  bddmulibl  25979  bddiblnc  25982  itggt0  25984  itgcn  25985  ellimc2  26017  limccnp  26031  limccnp2  26032  dvcobr  26086  lhop1  26154  elplyd  26340  coeeq2  26380  dvply1  26426  aalioulem3  26478  dvtaylp  26514  dvradcnv  26565  psercnlem1  26569  logcnlem2  26789  logcnlem3  26790  logcnlem4  26791  logtayllem  26805  logtayl  26806  cxpcl  26820  recxpcl  26821  leibpilem2  27087  leibpi  27088  rlimcnp2  27112  efrlim  27115  igamf  27196  igamcl  27197  pclogsum  27360  dchrelbasd  27384  lgsfcl2  27448  lgscllem  27449  lgsval2lem  27452  lgsne0  27480  2sqnn0  27583  dchrvmasumiflem2  27647  dchrisum0flblem1  27653  pntrlog2bndlem4  27725  pntrlog2bndlem5  27726  pntlemj  27748  padicabv  27775  crctcshwlkn0  30151  ccatws1f1o  33252  sgnsval  33462  elrgspnlem2  33544  elrgspnlem3  33545  elrgspnlem4  33546  gsummoncoe1fzo  33868  selvascl  33888  fldextrspunlsp  34045  extdgfialglem2  34064  xrge0iifcnv  34304  xrge0iifhom  34308  pnfneige0  34322  esumpinfval  34444  sigaclfu2  34492  ballotlemsv  34881  ballotlemsdom  34883  signswmnd  34925  signsvvf  34947  signsvfn  34950  mrsubcv  35983  mrsubff  35985  mrsubrn  35986  mrsubccat  35991  unblimceq0lem  37076  ptrecube  38252  poimirlem24  38276  itg2addnclem2  38304  itg2gt0cn  38307  ibladdnclem  38308  itgaddnclem1  38310  iblabsnclem  38315  iblabsnc  38316  iblmulc2nc  38317  itgmulc2nclem1  38318  itggt0cn  38322  ftc1anclem5  38329  ftc1anclem6  38330  ftc1anclem7  38331  ftc1anclem8  38332  ftc1anc  38333  areacirc  38345  cdleme27cl  41121  dffltz  43349  cantnfub  44031  climsuse  46307  lptioo1  46331  icccncfext  46584  cncfiooicclem1  46590  iblsplit  46663  dirkerval2  46791  dirkerre  46792  fourierdlem9  46813  fourierdlem17  46821  fourierdlem43  46847  etransclem3  46934  etransclem7  46938  etransclem10  46941  etransclem21  46952  lincext1  49217