Theorem ifclda 4459

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ifcif 4425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-if 4426

This theorem is referenced by:  unxpdomlem3  8708  updjudhf  9344  acndom  9462  iunfictbso  9525  dfac12lem2  9555  ttukeylem6  9925  canthp1lem2  10064  xaddf  12605  xmulf  12653  ccatcl  13917  swrdcl  13998  ccatco  14188  lo1bdd2  14873  o1lo1  14886  sadadd2lem2  15789  sadcaddlem  15796  sadadd2lem  15798  sadadd3  15800  lcmfval  15955  iserodd  16162  prmreclem2  16243  prmreclem4  16245  prmreclem6  16247  prmrec  16248  vdwlem6  16312  mreexexd  16911  smndex2hbas  18073  symgextf  18537  pmtrf  18575  odfval  18652  cyggex2  19010  dprdfid  19132  dmdprdsplitlem  19152  sdrgacs  19573  cygznlem1  20258  cygznlem2a  20259  cygznlem3  20261  cygth  20263  fvmptnn04if  21454  chfacfisf  21459  chfacfisfcpmat  21460  ptpjpre2  22185  ptopn2  22189  ptpjopn  22217  iccpnfcnv  23549  xrhmeo  23551  cmetcaulem  23892  ovolunlem1a  24100  ovolunlem1  24101  ioorf  24177  mbfi1fseqlem3  24321  mbfi1flim  24327  itg2seq  24346  itg2splitlem  24352  itg2split  24353  iblss  24408  itgle  24413  itgeqa  24417  ibladdlem  24423  itgaddlem1  24426  iblabslem  24431  iblabs  24432  iblabsr  24433  iblmulc2  24434  itgmulc2lem1  24435  bddmulibl  24442  bddiblnc  24445  itggt0  24447  itgcn  24448  ellimc2  24480  limccnp  24494  limccnp2  24495  dvcobr  24549  lhop1  24617  elplyd  24799  coeeq2  24839  dvply1  24880  aalioulem3  24930  dvtaylp  24965  dvradcnv  25016  psercnlem1  25020  logcnlem2  25234  logcnlem3  25235  logcnlem4  25236  logtayllem  25250  logtayl  25251  cxpcl  25265  recxpcl  25266  leibpilem2  25527  leibpi  25528  rlimcnp2  25552  efrlim  25555  igamf  25636  igamcl  25637  pclogsum  25799  dchrelbasd  25823  lgsfcl2  25887  lgscllem  25888  lgsval2lem  25891  lgsne0  25919  2sqnn0  26022  dchrvmasumiflem2  26086  dchrisum0flblem1  26092  pntrlog2bndlem4  26164  pntrlog2bndlem5  26165  pntlemj  26187  padicabv  26214  crctcshwlkn0  27607  sgnsval  30853  xrge0iifcnv  31286  xrge0iifhom  31290  pnfneige0  31304  esumpinfval  31442  sigaclfu2  31490  ballotlemsv  31877  ballotlemsdom  31879  signswmnd  31937  signsvvf  31959  signsvfn  31962  mrsubcv  32870  mrsubff  32872  mrsubrn  32873  mrsubccat  32878  unblimceq0lem  33958  ptrecube  35057  poimirlem24  35081  itg2addnclem2  35109  itg2gt0cn  35112  ibladdnclem  35113  itgaddnclem1  35115  iblabsnclem  35120  iblabsnc  35121  iblmulc2nc  35122  itgmulc2nclem1  35123  itggt0cn  35127  ftc1anclem5  35134  ftc1anclem6  35135  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  areacirc  35150  cdleme27cl  37662  selvval2lem5  39432  dffltz  39615  climsuse  42250  lptioo1  42274  icccncfext  42529  cncfiooicclem1  42535  iblsplit  42608  dirkerval2  42736  dirkerre  42737  fourierdlem9  42758  fourierdlem17  42766  fourierdlem43  42792  etransclem3  42879  etransclem7  42883  etransclem10  42886  etransclem21  42897  lincext1  44863