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

Theorem ifclda 3592
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 3571 . . . 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 2357 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  e.  C )
5 iffalse 3572 . . . 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 2357 . 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 1623    e. wcel 1684   ifcif 3565
This theorem is referenced by:  unxpdomlem3  7069  acndom  7678  iunfictbso  7741  dfac12lem2  7770  ttukeylem6  8141  canthp1lem2  8275  xaddf  10551  xmulf  10592  ccatcl  11429  swrdcl  11452  ccatco  11490  lo1bdd2  11998  o1lo1  12011  sadadd2lem2  12641  sadcaddlem  12648  sadadd2lem  12650  sadadd3  12652  iserodd  12888  prmreclem2  12964  prmreclem4  12966  prmreclem6  12968  prmrec  12969  vdwlem6  13033  cyggex2  15183  dprdfid  15252  dmdprdsplitlem  15272  cygznlem1  16520  cygznlem2a  16521  cygznlem3  16523  cygth  16525  ptpjpre2  17275  ptopn2  17279  ptpjopn  17306  iccpnfcnv  18442  xrhmeo  18444  cmetcaulem  18714  ovolunlem1a  18855  ovolunlem1  18856  ioorf  18928  mbfi1fseqlem3  19072  mbfi1flim  19078  itg2seq  19097  itg2splitlem  19103  itg2split  19104  iblss  19159  itgle  19164  itgeqa  19168  ibladdlem  19174  itgaddlem1  19177  iblabslem  19182  iblabs  19183  iblabsr  19184  iblmulc2  19185  itgmulc2lem1  19186  bddmulibl  19193  itggt0  19196  itgcn  19197  ellimc2  19227  limccnp  19241  limccnp2  19242  dvcobr  19295  lhop1  19361  elplyd  19584  coeeq2  19624  dvply1  19664  aalioulem3  19714  dvtaylp  19749  dvradcnv  19797  psercnlem1  19801  logcnlem2  19990  logcnlem3  19991  logcnlem4  19992  logtayllem  20006  logtayl  20007  cxpcl  20021  recxpcl  20022  leibpilem2  20237  leibpi  20238  rlimcnp2  20261  efrlim  20264  pclogsum  20454  dchrelbasd  20478  lgsfcl2  20541  lgscllem  20542  lgsval2lem  20545  lgsne0  20572  dchrvmasumiflem1  20650  dchrvmasumiflem2  20651  dchrisum0flblem1  20657  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntlemj  20752  padicabv  20779  ballotlemsv  23068  ballotlemsdom  23070  xrge0iifcnv  23315  pnfneige0  23374  esumpinfval  23441  sigaclfu2  23482  areacirc  24931  isconc2  26007  isconc3  26008  ifcldaOLD  26379  pmtrf  27397  sdrgacs  27509  climsuse  27734  cdleme27cl  30555
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-if 3566
  Copyright terms: Public domain W3C validator