Theorem ifclda 4512

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ifcif 4476

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-if 4477

This theorem is referenced by:  unxpdomlem3  9153  updjudhf  9835  acndom  9953  iunfictbso  10016  dfac12lem2  10047  ttukeylem6  10416  canthp1lem2  10555  xaddf  13130  xmulf  13178  ccatcl  14488  swrdcl  14560  ccatco  14749  lo1bdd2  15438  o1lo1  15451  sadadd2lem2  16368  sadcaddlem  16375  sadadd2lem  16377  sadadd3  16379  lcmfval  16539  iserodd  16754  prmreclem2  16836  prmreclem4  16838  prmreclem6  16840  prmrec  16841  vdwlem6  16905  mreexexd  17562  smndex2hbas  18832  symgextf  19337  pmtrf  19375  odfval  19452  cyggex2  19817  dprdfid  19939  dmdprdsplitlem  19959  sdrgacs  20725  cygznlem1  21512  cygznlem2a  21513  cygznlem3  21515  cygth  21517  fvmptnn04if  22784  chfacfisf  22789  chfacfisfcpmat  22790  ptpjpre2  23515  ptopn2  23519  ptpjopn  23547  iccpnfcnv  24889  xrhmeo  24891  cmetcaulem  25235  ovolunlem1a  25444  ovolunlem1  25445  ioorf  25521  mbfi1fseqlem3  25665  mbfi1flim  25671  itg2seq  25690  itg2splitlem  25696  itg2split  25697  iblss  25753  itgle  25758  itgeqa  25762  ibladdlem  25768  itgaddlem1  25771  iblabslem  25776  iblabs  25777  iblabsr  25778  iblmulc2  25779  itgmulc2lem1  25780  bddmulibl  25787  bddiblnc  25790  itggt0  25792  itgcn  25793  ellimc2  25825  limccnp  25839  limccnp2  25840  dvcobr  25896  dvcobrOLD  25897  lhop1  25966  elplyd  26154  coeeq2  26194  dvply1  26238  aalioulem3  26289  dvtaylp  26325  dvradcnv  26377  psercnlem1  26382  logcnlem2  26599  logcnlem3  26600  logcnlem4  26601  logtayllem  26615  logtayl  26616  cxpcl  26630  recxpcl  26631  leibpilem2  26898  leibpi  26899  rlimcnp2  26923  efrlim  26926  efrlimOLD  26927  igamf  27008  igamcl  27009  pclogsum  27173  dchrelbasd  27197  lgsfcl2  27261  lgscllem  27262  lgsval2lem  27265  lgsne0  27293  2sqnn0  27396  dchrvmasumiflem2  27460  dchrisum0flblem1  27466  pntrlog2bndlem4  27538  pntrlog2bndlem5  27539  pntlemj  27561  padicabv  27588  crctcshwlkn0  29820  ccatws1f1o  32961  sgnsval  33171  elrgspnlem2  33253  elrgspnlem3  33254  elrgspnlem4  33255  gsummoncoe1fzo  33606  fldextrspunlsp  33759  extdgfialglem2  33778  xrge0iifcnv  34018  xrge0iifhom  34022  pnfneige0  34036  esumpinfval  34158  sigaclfu2  34206  ballotlemsv  34595  ballotlemsdom  34597  signswmnd  34642  signsvvf  34664  signsvfn  34667  mrsubcv  35626  mrsubff  35628  mrsubrn  35629  mrsubccat  35634  unblimceq0lem  36622  ptrecube  37733  poimirlem24  37757  itg2addnclem2  37785  itg2gt0cn  37788  ibladdnclem  37789  itgaddnclem1  37791  iblabsnclem  37796  iblabsnc  37797  iblmulc2nc  37798  itgmulc2nclem1  37799  itggt0cn  37803  ftc1anclem5  37810  ftc1anclem6  37811  ftc1anclem7  37812  ftc1anclem8  37813  ftc1anc  37814  areacirc  37826  cdleme27cl  40538  selvcllem5  42740  selvvvval  42743  dffltz  42792  cantnfub  43478  climsuse  45770  lptioo1  45794  icccncfext  46047  cncfiooicclem1  46053  iblsplit  46126  dirkerval2  46254  dirkerre  46255  fourierdlem9  46276  fourierdlem17  46284  fourierdlem43  46310  etransclem3  46397  etransclem7  46401  etransclem10  46404  etransclem21  46415  lincext1  48616