Theorem ifclda 4120

Description: Conditional closure. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
ifclda.1	|- ( ( ph /\ ps ) -> A e. C )
ifclda.2	|- ( ( ph /\ -. ps ) -> B e. C )

Assertion

Ref	Expression
ifclda	|- ( ph -> if ( ps , A , B ) e. C )

Proof of Theorem ifclda

Step	Hyp	Ref	Expression
1		iftrue 4092	. . . 4 |- ( ps -> if ( ps , A , B ) = A )
2	1	adantl 482	. . 3 |- ( ( ph /\ ps ) -> if ( ps , A , B ) = A )
3		ifclda.1	. . 3 |- ( ( ph /\ ps ) -> A e. C )
4	2, 3	eqeltrd 2701	. 2 |- ( ( ph /\ ps ) -> if ( ps , A , B ) e. C )
5		iffalse 4095	. . . 4 |- ( -. ps -> if ( ps , A , B ) = B )
6	5	adantl 482	. . 3 |- ( ( ph /\ -. ps ) -> if ( ps , A , B ) = B )
7		ifclda.2	. . 3 |- ( ( ph /\ -. ps ) -> B e. C )
8	6, 7	eqeltrd 2701	. 2 |- ( ( ph /\ -. ps ) -> if ( ps , A , B ) e. C )
9	4, 8	pm2.61dan 832	1 |- ( ph -> if ( ps , A , B ) e. C )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  unxpdomlem3  8166  acndom  8874  iunfictbso  8937  dfac12lem2  8966  ttukeylem6  9336  canthp1lem2  9475  xaddf  12055  xmulf  12102  ccatcl  13359  swrdcl  13419  ccatco  13581  lo1bdd2  14255  o1lo1  14268  sadadd2lem2  15172  sadcaddlem  15179  sadadd2lem  15181  sadadd3  15183  lcmfval  15334  iserodd  15540  prmreclem2  15621  prmreclem4  15623  prmreclem6  15625  prmrec  15626  vdwlem6  15690  mreexexd  16308  symgextf  17837  pmtrf  17875  cyggex2  18298  dprdfid  18416  dmdprdsplitlem  18436  cygznlem1  19915  cygznlem2a  19916  cygznlem3  19918  cygth  19920  fvmptnn04if  20654  chfacfisf  20659  chfacfisfcpmat  20660  ptpjpre2  21383  ptopn2  21387  ptpjopn  21415  iccpnfcnv  22743  xrhmeo  22745  cmetcaulem  23086  ovolunlem1a  23264  ovolunlem1  23265  ioorf  23341  mbfi1fseqlem3  23484  mbfi1flim  23490  itg2seq  23509  itg2splitlem  23515  itg2split  23516  iblss  23571  itgle  23576  itgeqa  23580  ibladdlem  23586  itgaddlem1  23589  iblabslem  23594  iblabs  23595  iblabsr  23596  iblmulc2  23597  itgmulc2lem1  23598  bddmulibl  23605  itggt0  23608  itgcn  23609  ellimc2  23641  limccnp  23655  limccnp2  23656  dvcobr  23709  lhop1  23777  elplyd  23958  coeeq2  23998  dvply1  24039  aalioulem3  24089  dvtaylp  24124  dvradcnv  24175  psercnlem1  24179  logcnlem2  24389  logcnlem3  24390  logcnlem4  24391  logtayllem  24405  logtayl  24406  cxpcl  24420  recxpcl  24421  leibpilem2  24668  leibpi  24669  rlimcnp2  24693  efrlim  24696  igamf  24777  igamcl  24778  pclogsum  24940  dchrelbasd  24964  lgsfcl2  25028  lgscllem  25029  lgsval2lem  25032  lgsne0  25060  dchrvmasumiflem2  25191  dchrisum0flblem1  25197  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntlemj  25292  padicabv  25319  crctcshwlkn0  26713  sgnsval  29728  xrge0iifcnv  29979  xrge0iifhom  29983  pnfneige0  29997  esumpinfval  30135  sigaclfu2  30184  ballotlemsv  30571  ballotlemsdom  30573  signswmnd  30634  signsvvf  30656  signsvfn  30659  mrsubcv  31407  mrsubff  31409  mrsubrn  31410  mrsubccat  31415  unblimceq0lem  32497  ptrecube  33409  poimirlem24  33433  itg2addnclem2  33462  itg2gt0cn  33465  ibladdnclem  33466  itgaddnclem1  33468  iblabsnclem  33473  iblabsnc  33474  iblmulc2nc  33475  itgmulc2nclem1  33476  bddiblnc  33480  itggt0cn  33482  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  areacirc  33505  cdleme27cl  35654  sdrgacs  37771  climsuse  39840  lptioo1  39864  icccncfext  40100  cncfiooicclem1  40106  iblsplit  40182  dirkerval2  40311  dirkerre  40312  fourierdlem9  40333  fourierdlem17  40341  fourierdlem43  40367  etransclem3  40454  etransclem7  40458  etransclem10  40461  etransclem21  40472  lincext1  42243