Theorem ifclda 4525

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 4495	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 487	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifclda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2865	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5		iffalse 4498	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 487	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifclda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
8	6, 7	eqeltrd 2865	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
9	4, 8	pm2.61dan 825	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ifcif 4489

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4490

This theorem is used by:  unxpdomlem3  9221  updjudhf  9929  acndom  10047  iunfictbso  10110  dfac12lem2  10140  ttukeylem6  10509  canthp1lem2  10649  xaddf  13261  xmulf  13309  ccatcl  14624  swrdcl  14698  ccatco  14891  lo1bdd2  15594  o1lo1  15607  sadadd2lem2  16525  sadcaddlem  16532  sadadd2lem  16534  sadadd3  16536  lcmfval  16696  iserodd  16912  prmreclem2  16994  prmreclem4  16996  prmreclem6  16998  prmrec  16999  vdwlem6  17063  mreexexd  17721  smndex2hbas  19001  symgextf  19510  pmtrf  19548  odfval  19625  cyggex2  19990  dprdfid  20112  dmdprdsplitlem  20132  sdrgacs  20933  cygznlem1  21745  cygznlem2a  21746  cygznlem3  21748  cygth  21750  selvcllem5  22319  selvvvval  22322  fvmptnn04if  23035  chfacfisf  23040  chfacfisfcpmat  23041  ptpjpre2  23766  ptopn2  23770  ptpjopn  23798  iccpnfcnv  25132  xrhmeo  25134  cmetcaulem  25476  ovolunlem1a  25684  ovolunlem1  25685  ioorf  25761  mbfi1fseqlem3  25905  mbfi1flim  25911  itg2seq  25930  itg2splitlem  25936  itg2split  25937  iblss  25993  itgle  25998  itgeqa  26002  ibladdlem  26008  itgaddlem1  26011  iblabslem  26016  iblabs  26017  iblabsr  26018  iblmulc2  26019  itgmulc2lem1  26020  bddmulibl  26027  bddiblnc  26030  itggt0  26032  itgcn  26033  ellimc2  26065  limccnp  26079  limccnp2  26080  dvcobr  26134  lhop1  26202  elplyd  26388  coeeq2  26428  dvply1  26474  aalioulem3  26526  dvtaylp  26562  dvradcnv  26613  psercnlem1  26617  logcnlem2  26837  logcnlem3  26838  logcnlem4  26839  logtayllem  26853  logtayl  26854  cxpcl  26868  recxpcl  26869  leibpilem2  27135  leibpi  27136  rlimcnp2  27160  efrlim  27163  igamf  27244  igamcl  27245  pclogsum  27408  dchrelbasd  27432  lgsfcl2  27496  lgscllem  27497  lgsval2lem  27500  lgsne0  27528  2sqnn0  27631  dchrvmasumiflem2  27695  dchrisum0flblem1  27701  pntrlog2bndlem4  27773  pntrlog2bndlem5  27774  pntlemj  27796  padicabv  27823  crctcshwlkn0  30199  ccatws1f1o  33296  sgnsval  33504  elrgspnlem2  33586  elrgspnlem3  33587  elrgspnlem4  33588  gsummoncoe1fzo  33910  selvascl  33930  fldextrspunlsp  34087  extdgfialglem2  34106  xrge0iifcnv  34346  xrge0iifhom  34350  pnfneige0  34364  esumpinfval  34486  sigaclfu2  34534  ballotlemsv  34924  ballotlemsdom  34926  signswmnd  34968  signsvvf  34990  signsvfn  34993  mrsubcv  36015  mrsubff  36017  mrsubrn  36018  mrsubccat  36023  unblimceq0lem  37128  ptrecube  38304  poimirlem24  38328  itg2addnclem2  38356  itg2gt0cn  38359  ibladdnclem  38360  itgaddnclem1  38362  iblabsnclem  38367  iblabsnc  38368  iblmulc2nc  38369  itgmulc2nclem1  38370  itggt0cn  38374  ftc1anclem5  38381  ftc1anclem6  38382  ftc1anclem7  38383  ftc1anclem8  38384  ftc1anc  38385  areacirc  38397  cdleme27cl  41173  dffltz  43399  cantnfub  44081  climsuse  46357  lptioo1  46381  icccncfext  46634  cncfiooicclem1  46640  iblsplit  46713  dirkerval2  46841  dirkerre  46842  fourierdlem9  46863  fourierdlem17  46871  fourierdlem43  46897  etransclem3  46984  etransclem7  46988  etransclem10  46991  etransclem21  47002  lincext1  49267