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

Theorem ifclda 3766
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 3745 . . . 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 2510 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  e.  C )
5 iffalse 3746 . . . 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 2510 . 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 1652    e. wcel 1725   ifcif 3739
This theorem is referenced by:  unxpdomlem3  7315  acndom  7932  iunfictbso  7995  dfac12lem2  8024  ttukeylem6  8394  canthp1lem2  8528  xaddf  10810  xmulf  10851  ccatcl  11743  swrdcl  11766  ccatco  11804  lo1bdd2  12318  o1lo1  12331  sadadd2lem2  12962  sadcaddlem  12969  sadadd2lem  12971  sadadd3  12973  iserodd  13209  prmreclem2  13285  prmreclem4  13287  prmreclem6  13289  prmrec  13290  vdwlem6  13354  cyggex2  15506  dprdfid  15575  dmdprdsplitlem  15595  cygznlem1  16847  cygznlem2a  16848  cygznlem3  16850  cygth  16852  ptpjpre2  17612  ptopn2  17616  ptpjopn  17644  iccpnfcnv  18969  xrhmeo  18971  cmetcaulem  19241  ovolunlem1a  19392  ovolunlem1  19393  ioorf  19465  mbfi1fseqlem3  19609  mbfi1flim  19615  itg2seq  19634  itg2splitlem  19640  itg2split  19641  iblss  19696  itgle  19701  itgeqa  19705  ibladdlem  19711  itgaddlem1  19714  iblabslem  19719  iblabs  19720  iblabsr  19721  iblmulc2  19722  itgmulc2lem1  19723  bddmulibl  19730  itggt0  19733  itgcn  19734  ellimc2  19764  limccnp  19778  limccnp2  19779  dvcobr  19832  lhop1  19898  elplyd  20121  coeeq2  20161  dvply1  20201  aalioulem3  20251  dvtaylp  20286  dvradcnv  20337  psercnlem1  20341  logcnlem2  20534  logcnlem3  20535  logcnlem4  20536  logtayllem  20550  logtayl  20551  cxpcl  20565  recxpcl  20566  leibpilem2  20781  leibpi  20782  rlimcnp2  20805  efrlim  20808  pclogsum  20999  dchrelbasd  21023  lgsfcl2  21086  lgscllem  21087  lgsval2lem  21090  lgsne0  21117  dchrvmasumiflem1  21195  dchrvmasumiflem2  21196  dchrisum0flblem1  21202  pntrlog2bndlem4  21274  pntrlog2bndlem5  21275  pntlemj  21297  padicabv  21324  xrge0iifcnv  24319  xrge0iifhom  24323  pnfneige0  24336  esumpinfval  24463  sigaclfu2  24504  ballotlemsv  24767  ballotlemsdom  24769  igamf  24835  igamcl  24836  itg2addnclem2  26257  itg2gt0cn  26260  ibladdnclem  26261  itgaddnclem1  26263  iblabsnclem  26268  iblabsnc  26269  iblmulc2nc  26270  itgmulc2nclem1  26271  bddiblnc  26275  itggt0cn  26277  ftc1anclem5  26284  ftc1anclem6  26285  ftc1anclem7  26286  ftc1anclem8  26287  ftc1anc  26288  areacirc  26297  pmtrf  27374  sdrgacs  27486  climsuse  27710  cdleme27cl  31163
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-if 3740
  Copyright terms: Public domain W3C validator