Theorem ifclda 4567

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098  ifcif 4532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-if 4533

This theorem is referenced by:  unxpdomlem3  9283  updjudhf  9962  acndom  10082  iunfictbso  10145  dfac12lem2  10175  ttukeylem6  10545  canthp1lem2  10684  xaddf  13243  xmulf  13291  ccatcl  14564  swrdcl  14635  ccatco  14826  lo1bdd2  15508  o1lo1  15521  sadadd2lem2  16432  sadcaddlem  16439  sadadd2lem  16441  sadadd3  16443  lcmfval  16599  iserodd  16811  prmreclem2  16893  prmreclem4  16895  prmreclem6  16897  prmrec  16898  vdwlem6  16962  mreexexd  17635  smndex2hbas  18875  symgextf  19379  pmtrf  19417  odfval  19494  cyggex2  19859  dprdfid  19981  dmdprdsplitlem  20001  sdrgacs  20696  cygznlem1  21507  cygznlem2a  21508  cygznlem3  21510  cygth  21512  fvmptnn04if  22771  chfacfisf  22776  chfacfisfcpmat  22777  ptpjpre2  23504  ptopn2  23508  ptpjopn  23536  iccpnfcnv  24889  xrhmeo  24891  cmetcaulem  25236  ovolunlem1a  25445  ovolunlem1  25446  ioorf  25522  mbfi1fseqlem3  25667  mbfi1flim  25673  itg2seq  25692  itg2splitlem  25698  itg2split  25699  iblss  25754  itgle  25759  itgeqa  25763  ibladdlem  25769  itgaddlem1  25772  iblabslem  25777  iblabs  25778  iblabsr  25779  iblmulc2  25780  itgmulc2lem1  25781  bddmulibl  25788  bddiblnc  25791  itggt0  25793  itgcn  25794  ellimc2  25826  limccnp  25840  limccnp2  25841  dvcobr  25897  dvcobrOLD  25898  lhop1  25967  elplyd  26156  coeeq2  26196  dvply1  26238  aalioulem3  26289  dvtaylp  26325  dvradcnv  26377  psercnlem1  26382  logcnlem2  26597  logcnlem3  26598  logcnlem4  26599  logtayllem  26613  logtayl  26614  cxpcl  26628  recxpcl  26629  leibpilem2  26893  leibpi  26894  rlimcnp2  26918  efrlim  26921  efrlimOLD  26922  igamf  27003  igamcl  27004  pclogsum  27168  dchrelbasd  27192  lgsfcl2  27256  lgscllem  27257  lgsval2lem  27260  lgsne0  27288  2sqnn0  27391  dchrvmasumiflem2  27455  dchrisum0flblem1  27461  pntrlog2bndlem4  27533  pntrlog2bndlem5  27534  pntlemj  27556  padicabv  27583  crctcshwlkn0  29652  sgnsval  32903  gsummoncoe1fzo  33301  xrge0iifcnv  33567  xrge0iifhom  33571  pnfneige0  33585  esumpinfval  33725  sigaclfu2  33773  ballotlemsv  34162  ballotlemsdom  34164  signswmnd  34222  signsvvf  34244  signsvfn  34247  mrsubcv  35153  mrsubff  35155  mrsubrn  35156  mrsubccat  35161  unblimceq0lem  36014  ptrecube  37126  poimirlem24  37150  itg2addnclem2  37178  itg2gt0cn  37181  ibladdnclem  37182  itgaddnclem1  37184  iblabsnclem  37189  iblabsnc  37190  iblmulc2nc  37191  itgmulc2nclem1  37192  itggt0cn  37196  ftc1anclem5  37203  ftc1anclem6  37204  ftc1anclem7  37205  ftc1anclem8  37206  ftc1anc  37207  areacirc  37219  cdleme27cl  39871  selvcllem5  41846  selvvvval  41849  dffltz  42089  cantnfub  42781  climsuse  45025  lptioo1  45049  icccncfext  45304  cncfiooicclem1  45310  iblsplit  45383  dirkerval2  45511  dirkerre  45512  fourierdlem9  45533  fourierdlem17  45541  fourierdlem43  45567  etransclem3  45654  etransclem7  45658  etransclem10  45661  etransclem21  45672  lincext1  47600