MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifclda Unicode version

Theorem ifclda 3668
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
StepHypRef Expression
1 iftrue 3647 . . . 4  |-  ( ps 
->  if ( ps ,  A ,  B )  =  A )
21adantl 452 . . 3  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  =  A )
3 ifclda.1 . . 3  |-  ( (
ph  /\  ps )  ->  A  e.  C )
42, 3eqeltrd 2432 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  e.  C )
5 iffalse 3648 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  A ,  B
)  =  B )
65adantl 452 . . 3  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  =  B )
7 ifclda.2 . . 3  |-  ( (
ph  /\  -.  ps )  ->  B  e.  C )
86, 7eqeltrd 2432 . 2  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  e.  C )
94, 8pm2.61dan 766 1  |-  ( ph  ->  if ( ps ,  A ,  B )  e.  C )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358    = wceq 1642    e. wcel 1710   ifcif 3641
This theorem is referenced by:  unxpdomlem3  7157  acndom  7768  iunfictbso  7831  dfac12lem2  7860  ttukeylem6  8231  canthp1lem2  8365  xaddf  10643  xmulf  10684  ccatcl  11525  swrdcl  11548  ccatco  11586  lo1bdd2  12094  o1lo1  12107  sadadd2lem2  12738  sadcaddlem  12745  sadadd2lem  12747  sadadd3  12749  iserodd  12985  prmreclem2  13061  prmreclem4  13063  prmreclem6  13065  prmrec  13066  vdwlem6  13130  cyggex2  15282  dprdfid  15351  dmdprdsplitlem  15371  cygznlem1  16626  cygznlem2a  16627  cygznlem3  16629  cygth  16631  ptpjpre2  17381  ptopn2  17385  ptpjopn  17412  iccpnfcnv  18546  xrhmeo  18548  cmetcaulem  18818  ovolunlem1a  18959  ovolunlem1  18960  ioorf  19032  mbfi1fseqlem3  19176  mbfi1flim  19182  itg2seq  19201  itg2splitlem  19207  itg2split  19208  iblss  19263  itgle  19268  itgeqa  19272  ibladdlem  19278  itgaddlem1  19281  iblabslem  19286  iblabs  19287  iblabsr  19288  iblmulc2  19289  itgmulc2lem1  19290  bddmulibl  19297  itggt0  19300  itgcn  19301  ellimc2  19331  limccnp  19345  limccnp2  19346  dvcobr  19399  lhop1  19465  elplyd  19688  coeeq2  19728  dvply1  19768  aalioulem3  19818  dvtaylp  19853  dvradcnv  19904  psercnlem1  19908  logcnlem2  20101  logcnlem3  20102  logcnlem4  20103  logtayllem  20117  logtayl  20118  cxpcl  20132  recxpcl  20133  leibpilem2  20348  leibpi  20349  rlimcnp2  20372  efrlim  20375  pclogsum  20566  dchrelbasd  20590  lgsfcl2  20653  lgscllem  20654  lgsval2lem  20657  lgsne0  20684  dchrvmasumiflem1  20762  dchrvmasumiflem2  20763  dchrisum0flblem1  20769  pntrlog2bndlem4  20841  pntrlog2bndlem5  20842  pntlemj  20864  padicabv  20891  xrge0iifcnv  23475  pnfneige0  23492  esumpinfval  23729  sigaclfu2  23770  ballotlemsv  24016  ballotlemsdom  24018  igamf  24084  igamcl  24085  itg2addnclem2  25493  itg2gt0cn  25495  ibladdnclem  25496  itgaddnclem1  25498  iblabsnclem  25503  iblabsnc  25504  iblmulc2nc  25505  itgmulc2nclem1  25506  bddiblnc  25510  itggt0cn  25512  areacirc  25523  ifcldaOLD  25703  pmtrf  26720  sdrgacs  26832  climsuse  27057  cdleme27cl  30624
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-if 3642
  Copyright terms: Public domain W3C validator