Theorem ifclda 4503

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ifcif 4469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-if 4470

This theorem is referenced by:  unxpdomlem3  8726  updjudhf  9362  acndom  9479  iunfictbso  9542  dfac12lem2  9572  ttukeylem6  9938  canthp1lem2  10077  xaddf  12620  xmulf  12668  ccatcl  13928  swrdcl  14009  ccatco  14199  lo1bdd2  14883  o1lo1  14896  sadadd2lem2  15801  sadcaddlem  15808  sadadd2lem  15810  sadadd3  15812  lcmfval  15967  iserodd  16174  prmreclem2  16255  prmreclem4  16257  prmreclem6  16259  prmrec  16260  vdwlem6  16324  mreexexd  16921  smndex2hbas  18083  symgextf  18547  pmtrf  18585  odfval  18662  cyggex2  19019  dprdfid  19141  dmdprdsplitlem  19161  sdrgacs  19582  cygznlem1  20715  cygznlem2a  20716  cygznlem3  20718  cygth  20720  fvmptnn04if  21459  chfacfisf  21464  chfacfisfcpmat  21465  ptpjpre2  22190  ptopn2  22194  ptpjopn  22222  iccpnfcnv  23550  xrhmeo  23552  cmetcaulem  23893  ovolunlem1a  24099  ovolunlem1  24100  ioorf  24176  mbfi1fseqlem3  24320  mbfi1flim  24326  itg2seq  24345  itg2splitlem  24351  itg2split  24352  iblss  24407  itgle  24412  itgeqa  24416  ibladdlem  24422  itgaddlem1  24425  iblabslem  24430  iblabs  24431  iblabsr  24432  iblmulc2  24433  itgmulc2lem1  24434  bddmulibl  24441  itggt0  24444  itgcn  24445  ellimc2  24477  limccnp  24491  limccnp2  24492  dvcobr  24545  lhop1  24613  elplyd  24794  coeeq2  24834  dvply1  24875  aalioulem3  24925  dvtaylp  24960  dvradcnv  25011  psercnlem1  25015  logcnlem2  25228  logcnlem3  25229  logcnlem4  25230  logtayllem  25244  logtayl  25245  cxpcl  25259  recxpcl  25260  leibpilem2  25521  leibpi  25522  rlimcnp2  25546  efrlim  25549  igamf  25630  igamcl  25631  pclogsum  25793  dchrelbasd  25817  lgsfcl2  25881  lgscllem  25882  lgsval2lem  25885  lgsne0  25913  2sqnn0  26016  dchrvmasumiflem2  26080  dchrisum0flblem1  26086  pntrlog2bndlem4  26158  pntrlog2bndlem5  26159  pntlemj  26181  padicabv  26208  crctcshwlkn0  27601  sgnsval  30805  xrge0iifcnv  31178  xrge0iifhom  31182  pnfneige0  31196  esumpinfval  31334  sigaclfu2  31382  ballotlemsv  31769  ballotlemsdom  31771  signswmnd  31829  signsvvf  31851  signsvfn  31854  mrsubcv  32759  mrsubff  32761  mrsubrn  32762  mrsubccat  32767  unblimceq0lem  33847  ptrecube  34894  poimirlem24  34918  itg2addnclem2  34946  itg2gt0cn  34949  ibladdnclem  34950  itgaddnclem1  34952  iblabsnclem  34957  iblabsnc  34958  iblmulc2nc  34959  itgmulc2nclem1  34960  bddiblnc  34964  itggt0cn  34966  ftc1anclem5  34973  ftc1anclem6  34974  ftc1anclem7  34975  ftc1anclem8  34976  ftc1anc  34977  areacirc  34989  cdleme27cl  37504  selvval2lem5  39144  dffltz  39278  climsuse  41896  lptioo1  41920  icccncfext  42177  cncfiooicclem1  42183  iblsplit  42258  dirkerval2  42386  dirkerre  42387  fourierdlem9  42408  fourierdlem17  42416  fourierdlem43  42442  etransclem3  42529  etransclem7  42533  etransclem10  42536  etransclem21  42547  lincext1  44516