Theorem ifclda 4500

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   = wceq 1533   ∈ wcel 2110  ifcif 4466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-if 4467

This theorem is referenced by:  unxpdomlem3  8718  updjudhf  9354  acndom  9471  iunfictbso  9534  dfac12lem2  9564  ttukeylem6  9930  canthp1lem2  10069  xaddf  12611  xmulf  12659  ccatcl  13920  swrdcl  14001  ccatco  14191  lo1bdd2  14875  o1lo1  14888  sadadd2lem2  15793  sadcaddlem  15800  sadadd2lem  15802  sadadd3  15804  lcmfval  15959  iserodd  16166  prmreclem2  16247  prmreclem4  16249  prmreclem6  16251  prmrec  16252  vdwlem6  16316  mreexexd  16913  smndex2hbas  18075  symgextf  18539  pmtrf  18577  odfval  18654  cyggex2  19011  dprdfid  19133  dmdprdsplitlem  19153  sdrgacs  19574  cygznlem1  20707  cygznlem2a  20708  cygznlem3  20710  cygth  20712  fvmptnn04if  21451  chfacfisf  21456  chfacfisfcpmat  21457  ptpjpre2  22182  ptopn2  22186  ptpjopn  22214  iccpnfcnv  23542  xrhmeo  23544  cmetcaulem  23885  ovolunlem1a  24091  ovolunlem1  24092  ioorf  24168  mbfi1fseqlem3  24312  mbfi1flim  24318  itg2seq  24337  itg2splitlem  24343  itg2split  24344  iblss  24399  itgle  24404  itgeqa  24408  ibladdlem  24414  itgaddlem1  24417  iblabslem  24422  iblabs  24423  iblabsr  24424  iblmulc2  24425  itgmulc2lem1  24426  bddmulibl  24433  itggt0  24436  itgcn  24437  ellimc2  24469  limccnp  24483  limccnp2  24484  dvcobr  24537  lhop1  24605  elplyd  24786  coeeq2  24826  dvply1  24867  aalioulem3  24917  dvtaylp  24952  dvradcnv  25003  psercnlem1  25007  logcnlem2  25220  logcnlem3  25221  logcnlem4  25222  logtayllem  25236  logtayl  25237  cxpcl  25251  recxpcl  25252  leibpilem2  25513  leibpi  25514  rlimcnp2  25538  efrlim  25541  igamf  25622  igamcl  25623  pclogsum  25785  dchrelbasd  25809  lgsfcl2  25873  lgscllem  25874  lgsval2lem  25877  lgsne0  25905  2sqnn0  26008  dchrvmasumiflem2  26072  dchrisum0flblem1  26078  pntrlog2bndlem4  26150  pntrlog2bndlem5  26151  pntlemj  26173  padicabv  26200  crctcshwlkn0  27593  sgnsval  30798  xrge0iifcnv  31171  xrge0iifhom  31175  pnfneige0  31189  esumpinfval  31327  sigaclfu2  31375  ballotlemsv  31762  ballotlemsdom  31764  signswmnd  31822  signsvvf  31844  signsvfn  31847  mrsubcv  32752  mrsubff  32754  mrsubrn  32755  mrsubccat  32760  unblimceq0lem  33840  ptrecube  34886  poimirlem24  34910  itg2addnclem2  34938  itg2gt0cn  34941  ibladdnclem  34942  itgaddnclem1  34944  iblabsnclem  34949  iblabsnc  34950  iblmulc2nc  34951  itgmulc2nclem1  34952  bddiblnc  34956  itggt0cn  34958  ftc1anclem5  34965  ftc1anclem6  34966  ftc1anclem7  34967  ftc1anclem8  34968  ftc1anc  34969  areacirc  34981  cdleme27cl  37496  selvval2lem5  39130  dffltz  39264  climsuse  41882  lptioo1  41906  icccncfext  42163  cncfiooicclem1  42169  iblsplit  42244  dirkerval2  42373  dirkerre  42374  fourierdlem9  42395  fourierdlem17  42403  fourierdlem43  42429  etransclem3  42516  etransclem7  42520  etransclem10  42523  etransclem21  42534  lincext1  44503