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

Theorem ifclda 3833
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 3809 . . . 4  |-  ( ps 
->  if ( ps ,  A ,  B )  =  A )
21adantl 466 . . 3  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  =  A )
3 ifclda.1 . . 3  |-  ( (
ph  /\  ps )  ->  A  e.  C )
42, 3eqeltrd 2517 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  e.  C )
5 iffalse 3811 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  A ,  B
)  =  B )
65adantl 466 . . 3  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  =  B )
7 ifclda.2 . . 3  |-  ( (
ph  /\  -.  ps )  ->  B  e.  C )
86, 7eqeltrd 2517 . 2  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  e.  C )
94, 8pm2.61dan 789 1  |-  ( ph  ->  if ( ps ,  A ,  B )  e.  C )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   ifcif 3803
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-if 3804
This theorem is referenced by:  unxpdomlem3  7531  acndom  8233  iunfictbso  8296  dfac12lem2  8325  ttukeylem6  8695  canthp1lem2  8832  xaddf  11206  xmulf  11247  ccatcl  12286  swrdcl  12327  ccatco  12475  lo1bdd2  13014  o1lo1  13027  sadadd2lem2  13658  sadcaddlem  13665  sadadd2lem  13667  sadadd3  13669  iserodd  13914  prmreclem2  13990  prmreclem4  13992  prmreclem6  13994  prmrec  13995  vdwlem6  14059  symgextf  15934  pmtrf  15973  cyggex2  16385  dprdfid  16519  dprdfidOLD  16526  dmdprdsplitlem  16546  dmdprdsplitlemOLD  16547  cygznlem1  18011  cygznlem2a  18012  cygznlem3  18014  cygth  18016  ptpjpre2  19165  ptopn2  19169  ptpjopn  19197  iccpnfcnv  20528  xrhmeo  20530  cmetcaulem  20811  ovolunlem1a  20991  ovolunlem1  20992  ioorf  21065  mbfi1fseqlem3  21207  mbfi1flim  21213  itg2seq  21232  itg2splitlem  21238  itg2split  21239  iblss  21294  itgle  21299  itgeqa  21303  ibladdlem  21309  itgaddlem1  21312  iblabslem  21317  iblabs  21318  iblabsr  21319  iblmulc2  21320  itgmulc2lem1  21321  bddmulibl  21328  itggt0  21331  itgcn  21332  ellimc2  21364  limccnp  21378  limccnp2  21379  dvcobr  21432  lhop1  21498  elplyd  21682  coeeq2  21722  dvply1  21762  aalioulem3  21812  dvtaylp  21847  dvradcnv  21898  psercnlem1  21902  logcnlem2  22100  logcnlem3  22101  logcnlem4  22102  logtayllem  22116  logtayl  22117  cxpcl  22131  recxpcl  22132  leibpilem2  22348  leibpi  22349  rlimcnp2  22372  efrlim  22375  pclogsum  22566  dchrelbasd  22590  lgsfcl2  22653  lgscllem  22654  lgsval2lem  22657  lgsne0  22684  dchrvmasumiflem1  22762  dchrvmasumiflem2  22763  dchrisum0flblem1  22769  pntrlog2bndlem4  22841  pntrlog2bndlem5  22842  pntlemj  22864  padicabv  22891  sgnsval  26203  xrge0iifcnv  26375  xrge0iifhom  26379  pnfneige0  26393  esumpinfval  26534  sigaclfu2  26576  ballotlemsv  26904  ballotlemsdom  26906  signsvvf  26992  signsvfn  26995  igamf  27049  igamcl  27050  itg2addnclem2  28456  itg2gt0cn  28459  ibladdnclem  28460  itgaddnclem1  28462  iblabsnclem  28467  iblabsnc  28468  iblmulc2nc  28469  itgmulc2nclem1  28470  bddiblnc  28474  itggt0cn  28476  ftc1anclem5  28483  ftc1anclem6  28484  ftc1anclem7  28485  ftc1anclem8  28486  ftc1anc  28487  areacirc  28501  sdrgacs  29570  climsuse  29793  lincext1  31000  cdleme27cl  34022
  Copyright terms: Public domain W3C validator