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

Theorem ifclda 3726
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 3705 . . . 4  |-  ( ps 
->  if ( ps ,  A ,  B )  =  A )
21adantl 453 . . 3  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  =  A )
3 ifclda.1 . . 3  |-  ( (
ph  /\  ps )  ->  A  e.  C )
42, 3eqeltrd 2478 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  e.  C )
5 iffalse 3706 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  A ,  B
)  =  B )
65adantl 453 . . 3  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  =  B )
7 ifclda.2 . . 3  |-  ( (
ph  /\  -.  ps )  ->  B  e.  C )
86, 7eqeltrd 2478 . 2  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  e.  C )
94, 8pm2.61dan 767 1  |-  ( ph  ->  if ( ps ,  A ,  B )  e.  C )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721   ifcif 3699
This theorem is referenced by:  unxpdomlem3  7274  acndom  7888  iunfictbso  7951  dfac12lem2  7980  ttukeylem6  8350  canthp1lem2  8484  xaddf  10766  xmulf  10807  ccatcl  11698  swrdcl  11721  ccatco  11759  lo1bdd2  12273  o1lo1  12286  sadadd2lem2  12917  sadcaddlem  12924  sadadd2lem  12926  sadadd3  12928  iserodd  13164  prmreclem2  13240  prmreclem4  13242  prmreclem6  13244  prmrec  13245  vdwlem6  13309  cyggex2  15461  dprdfid  15530  dmdprdsplitlem  15550  cygznlem1  16802  cygznlem2a  16803  cygznlem3  16805  cygth  16807  ptpjpre2  17565  ptopn2  17569  ptpjopn  17597  iccpnfcnv  18922  xrhmeo  18924  cmetcaulem  19194  ovolunlem1a  19345  ovolunlem1  19346  ioorf  19418  mbfi1fseqlem3  19562  mbfi1flim  19568  itg2seq  19587  itg2splitlem  19593  itg2split  19594  iblss  19649  itgle  19654  itgeqa  19658  ibladdlem  19664  itgaddlem1  19667  iblabslem  19672  iblabs  19673  iblabsr  19674  iblmulc2  19675  itgmulc2lem1  19676  bddmulibl  19683  itggt0  19686  itgcn  19687  ellimc2  19717  limccnp  19731  limccnp2  19732  dvcobr  19785  lhop1  19851  elplyd  20074  coeeq2  20114  dvply1  20154  aalioulem3  20204  dvtaylp  20239  dvradcnv  20290  psercnlem1  20294  logcnlem2  20487  logcnlem3  20488  logcnlem4  20489  logtayllem  20503  logtayl  20504  cxpcl  20518  recxpcl  20519  leibpilem2  20734  leibpi  20735  rlimcnp2  20758  efrlim  20761  pclogsum  20952  dchrelbasd  20976  lgsfcl2  21039  lgscllem  21040  lgsval2lem  21043  lgsne0  21070  dchrvmasumiflem1  21148  dchrvmasumiflem2  21149  dchrisum0flblem1  21155  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntlemj  21250  padicabv  21277  xrge0iifcnv  24272  xrge0iifhom  24276  pnfneige0  24289  esumpinfval  24416  sigaclfu2  24457  ballotlemsv  24720  ballotlemsdom  24722  igamf  24788  igamcl  24789  itg2addnclem2  26156  itg2gt0cn  26159  ibladdnclem  26160  itgaddnclem1  26162  iblabsnclem  26167  iblabsnc  26168  iblmulc2nc  26169  itgmulc2nclem1  26170  bddiblnc  26174  itggt0cn  26176  areacirc  26187  pmtrf  27265  sdrgacs  27377  climsuse  27601  cdleme27cl  30848
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-if 3700
  Copyright terms: Public domain W3C validator