Theorem ifclda 4513

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 4483	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 485	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifclda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2861	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5		iffalse 4486	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 485	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifclda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
8	6, 7	eqeltrd 2861	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
9	4, 8	pm2.61dan 822	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  ifcif 4477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4478

This theorem is referenced by:  unxpdomlem3  9196  updjudhf  9883  acndom  10001  iunfictbso  10064  dfac12lem2  10095  ttukeylem6  10465  canthp1lem2  10605  xaddf  13221  xmulf  13269  ccatcl  14581  swrdcl  14653  ccatco  14842  lo1bdd2  15542  o1lo1  15555  sadadd2lem2  16475  sadcaddlem  16482  sadadd2lem  16484  sadadd3  16486  lcmfval  16646  iserodd  16862  prmreclem2  16944  prmreclem4  16946  prmreclem6  16948  prmrec  16949  vdwlem6  17013  mreexexd  17671  smndex2hbas  18944  symgextf  19448  pmtrf  19486  odfval  19563  cyggex2  19928  dprdfid  20050  dmdprdsplitlem  20070  sdrgacs  20838  cygznlem1  21606  cygznlem2a  21607  cygznlem3  21609  cygth  21611  selvcllem5  22180  selvvvval  22183  fvmptnn04if  22897  chfacfisf  22902  chfacfisfcpmat  22903  ptpjpre2  23628  ptopn2  23632  ptpjopn  23660  iccpnfcnv  24994  xrhmeo  24996  cmetcaulem  25338  ovolunlem1a  25546  ovolunlem1  25547  ioorf  25623  mbfi1fseqlem3  25767  mbfi1flim  25773  itg2seq  25792  itg2splitlem  25798  itg2split  25799  iblss  25855  itgle  25860  itgeqa  25864  ibladdlem  25870  itgaddlem1  25873  iblabslem  25878  iblabs  25879  iblabsr  25880  iblmulc2  25881  itgmulc2lem1  25882  bddmulibl  25889  bddiblnc  25892  itggt0  25894  itgcn  25895  ellimc2  25927  limccnp  25941  limccnp2  25942  dvcobr  25996  lhop1  26064  elplyd  26250  coeeq2  26290  dvply1  26336  aalioulem3  26386  dvtaylp  26421  dvradcnv  26472  psercnlem1  26476  logcnlem2  26696  logcnlem3  26697  logcnlem4  26698  logtayllem  26712  logtayl  26713  cxpcl  26727  recxpcl  26728  leibpilem2  26994  leibpi  26995  rlimcnp2  27019  efrlim  27022  igamf  27103  igamcl  27104  pclogsum  27267  dchrelbasd  27291  lgsfcl2  27355  lgscllem  27356  lgsval2lem  27359  lgsne0  27387  2sqnn0  27490  dchrvmasumiflem2  27554  dchrisum0flblem1  27560  pntrlog2bndlem4  27632  pntrlog2bndlem5  27633  pntlemj  27655  padicabv  27682  crctcshwlkn0  29978  ccatws1f1o  33090  sgnsval  33302  elrgspnlem2  33385  elrgspnlem3  33386  elrgspnlem4  33387  gsummoncoe1fzo  33754  selvascl  33775  fldextrspunlsp  33932  extdgfialglem2  33951  xrge0iifcnv  34191  xrge0iifhom  34195  pnfneige0  34209  esumpinfval  34331  sigaclfu2  34379  ballotlemsv  34768  ballotlemsdom  34770  signswmnd  34812  signsvvf  34834  signsvfn  34837  mrsubcv  35821  mrsubff  35823  mrsubrn  35824  mrsubccat  35829  unblimceq0lem  36905  ptrecube  38080  poimirlem24  38104  itg2addnclem2  38132  itg2gt0cn  38135  ibladdnclem  38136  itgaddnclem1  38138  iblabsnclem  38143  iblabsnc  38144  iblmulc2nc  38145  itgmulc2nclem1  38146  itggt0cn  38150  ftc1anclem5  38157  ftc1anclem6  38158  ftc1anclem7  38159  ftc1anclem8  38160  ftc1anc  38161  areacirc  38173  cdleme27cl  40951  dffltz  43177  cantnfub  43859  climsuse  46145  lptioo1  46169  icccncfext  46422  cncfiooicclem1  46428  iblsplit  46501  dirkerval2  46629  dirkerre  46630  fourierdlem9  46651  fourierdlem17  46659  fourierdlem43  46685  etransclem3  46772  etransclem7  46776  etransclem10  46779  etransclem21  46790  lincext1  49037