Theorem ifclda 4339

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 4311	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 475	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifclda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2905	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5		iffalse 4314	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 475	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifclda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
8	6, 7	eqeltrd 2905	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
9	4, 8	pm2.61dan 849	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 386   = wceq 1658   ∈ wcel 2166  ifcif 4305

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2802

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-if 4306

This theorem is referenced by:  unxpdomlem3  8434  updjudhf  9069  acndom  9186  iunfictbso  9249  dfac12lem2  9280  ttukeylem6  9650  canthp1lem2  9789  xaddf  12342  xmulf  12389  ccatcl  13633  swrdcl  13704  ccatco  13955  lo1bdd2  14631  o1lo1  14644  sadadd2lem2  15544  sadcaddlem  15551  sadadd2lem  15553  sadadd3  15555  lcmfval  15706  iserodd  15910  prmreclem2  15991  prmreclem4  15993  prmreclem6  15995  prmrec  15996  vdwlem6  16060  mreexexd  16660  symgextf  18186  pmtrf  18224  cyggex2  18650  dprdfid  18769  dmdprdsplitlem  18789  cygznlem1  20273  cygznlem2a  20274  cygznlem3  20276  cygth  20278  fvmptnn04if  21023  chfacfisf  21028  chfacfisfcpmat  21029  ptpjpre2  21753  ptopn2  21757  ptpjopn  21785  iccpnfcnv  23112  xrhmeo  23114  cmetcaulem  23455  ovolunlem1a  23661  ovolunlem1  23662  ioorf  23738  mbfi1fseqlem3  23882  mbfi1flim  23888  itg2seq  23907  itg2splitlem  23913  itg2split  23914  iblss  23969  itgle  23974  itgeqa  23978  ibladdlem  23984  itgaddlem1  23987  iblabslem  23992  iblabs  23993  iblabsr  23994  iblmulc2  23995  itgmulc2lem1  23996  bddmulibl  24003  itggt0  24006  itgcn  24007  ellimc2  24039  limccnp  24053  limccnp2  24054  dvcobr  24107  lhop1  24175  elplyd  24356  coeeq2  24396  dvply1  24437  aalioulem3  24487  dvtaylp  24522  dvradcnv  24573  psercnlem1  24577  logcnlem2  24787  logcnlem3  24788  logcnlem4  24789  logtayllem  24803  logtayl  24804  cxpcl  24818  recxpcl  24819  leibpilem2  25080  leibpi  25081  rlimcnp2  25105  efrlim  25108  igamf  25189  igamcl  25190  pclogsum  25352  dchrelbasd  25376  lgsfcl2  25440  lgscllem  25441  lgsval2lem  25444  lgsne0  25472  dchrvmasumiflem2  25603  dchrisum0flblem1  25609  pntrlog2bndlem4  25681  pntrlog2bndlem5  25682  pntlemj  25704  padicabv  25731  crctcshwlkn0  27119  sgnsval  30272  xrge0iifcnv  30523  xrge0iifhom  30527  pnfneige0  30541  esumpinfval  30679  sigaclfu2  30728  ballotlemsv  31116  ballotlemsdom  31118  signswmnd  31180  signsvvf  31204  signsvfn  31207  mrsubcv  31952  mrsubff  31954  mrsubrn  31955  mrsubccat  31960  unblimceq0lem  33028  ptrecube  33952  poimirlem24  33976  itg2addnclem2  34004  itg2gt0cn  34007  ibladdnclem  34008  itgaddnclem1  34010  iblabsnclem  34015  iblabsnc  34016  iblmulc2nc  34017  itgmulc2nclem1  34018  bddiblnc  34022  itggt0cn  34024  ftc1anclem5  34031  ftc1anclem6  34032  ftc1anclem7  34033  ftc1anclem8  34034  ftc1anc  34035  areacirc  34047  cdleme27cl  36440  dffltz  38096  sdrgacs  38613  climsuse  40634  lptioo1  40658  icccncfext  40894  cncfiooicclem1  40900  iblsplit  40975  dirkerval2  41104  dirkerre  41105  fourierdlem9  41126  fourierdlem17  41134  fourierdlem43  41160  etransclem3  41247  etransclem7  41251  etransclem10  41254  etransclem21  41265  lincext1  43089