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

Theorem ifclda 3594
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 3573 . . . 4  |-  ( ps 
->  if ( ps ,  A ,  B )  =  A )
21adantl 454 . . 3  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  =  A )
3 ifclda.1 . . 3  |-  ( (
ph  /\  ps )  ->  A  e.  C )
42, 3eqeltrd 2359 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  e.  C )
5 iffalse 3574 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  A ,  B
)  =  B )
65adantl 454 . . 3  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  =  B )
7 ifclda.2 . . 3  |-  ( (
ph  /\  -.  ps )  ->  B  e.  C )
86, 7eqeltrd 2359 . 2  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  e.  C )
94, 8pm2.61dan 768 1  |-  ( ph  ->  if ( ps ,  A ,  B )  e.  C )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    /\ wa 360    = wceq 1624    e. wcel 1685   ifcif 3567
This theorem is referenced by:  unxpdomlem3  7065  acndom  7674  iunfictbso  7737  dfac12lem2  7766  ttukeylem6  8137  canthp1lem2  8271  xaddf  10546  xmulf  10587  ccatcl  11424  swrdcl  11447  ccatco  11485  lo1bdd2  11993  o1lo1  12006  sadadd2lem2  12636  sadcaddlem  12643  sadadd2lem  12645  sadadd3  12647  iserodd  12883  prmreclem2  12959  prmreclem4  12961  prmreclem6  12963  prmrec  12964  vdwlem6  13028  cyggex2  15178  dprdfid  15247  dmdprdsplitlem  15267  cygznlem1  16515  cygznlem2a  16516  cygznlem3  16518  cygth  16520  ptpjpre2  17270  ptopn2  17274  ptpjopn  17301  iccpnfcnv  18437  xrhmeo  18439  cmetcaulem  18709  ovolunlem1a  18850  ovolunlem1  18851  ioorf  18923  mbfi1fseqlem3  19067  mbfi1flim  19073  itg2seq  19092  itg2splitlem  19098  itg2split  19099  iblss  19154  itgle  19159  itgeqa  19163  ibladdlem  19169  itgaddlem1  19172  iblabslem  19177  iblabs  19178  iblabsr  19179  iblmulc2  19180  itgmulc2lem1  19181  bddmulibl  19188  itggt0  19191  itgcn  19192  ellimc2  19222  limccnp  19236  limccnp2  19237  dvcobr  19290  lhop1  19356  elplyd  19579  coeeq2  19619  dvply1  19659  aalioulem3  19709  dvtaylp  19744  dvradcnv  19792  psercnlem1  19796  logcnlem2  19985  logcnlem3  19986  logcnlem4  19987  logtayllem  20001  logtayl  20002  cxpcl  20016  recxpcl  20017  leibpilem2  20232  leibpi  20233  rlimcnp2  20256  efrlim  20259  pclogsum  20449  dchrelbasd  20473  lgsfcl2  20536  lgscllem  20537  lgsval2lem  20540  lgsne0  20567  dchrvmasumiflem1  20645  dchrvmasumiflem2  20646  dchrisum0flblem1  20652  pntrlog2bndlem4  20724  pntrlog2bndlem5  20725  pntlemj  20747  padicabv  20774  ballotlemsv  23062  ballotlemsdom  23064  isconc2  25407  isconc3  25408  ifcldaOLD  25779  pmtrf  26797  sdrgacs  26909  climsuse  27134  cdleme27cl  29823
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-if 3568
  Copyright terms: Public domain W3C validator