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

Theorem ifclda 3758
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 3737 . . . 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 2509 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  e.  C )
5 iffalse 3738 . . . 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 2509 . 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 3731
This theorem is referenced by:  unxpdomlem3  7306  acndom  7921  iunfictbso  7984  dfac12lem2  8013  ttukeylem6  8383  canthp1lem2  8517  xaddf  10799  xmulf  10840  ccatcl  11731  swrdcl  11754  ccatco  11792  lo1bdd2  12306  o1lo1  12319  sadadd2lem2  12950  sadcaddlem  12957  sadadd2lem  12959  sadadd3  12961  iserodd  13197  prmreclem2  13273  prmreclem4  13275  prmreclem6  13277  prmrec  13278  vdwlem6  13342  cyggex2  15494  dprdfid  15563  dmdprdsplitlem  15583  cygznlem1  16835  cygznlem2a  16836  cygznlem3  16838  cygth  16840  ptpjpre2  17600  ptopn2  17604  ptpjopn  17632  iccpnfcnv  18957  xrhmeo  18959  cmetcaulem  19229  ovolunlem1a  19380  ovolunlem1  19381  ioorf  19453  mbfi1fseqlem3  19597  mbfi1flim  19603  itg2seq  19622  itg2splitlem  19628  itg2split  19629  iblss  19684  itgle  19689  itgeqa  19693  ibladdlem  19699  itgaddlem1  19702  iblabslem  19707  iblabs  19708  iblabsr  19709  iblmulc2  19710  itgmulc2lem1  19711  bddmulibl  19718  itggt0  19721  itgcn  19722  ellimc2  19752  limccnp  19766  limccnp2  19767  dvcobr  19820  lhop1  19886  elplyd  20109  coeeq2  20149  dvply1  20189  aalioulem3  20239  dvtaylp  20274  dvradcnv  20325  psercnlem1  20329  logcnlem2  20522  logcnlem3  20523  logcnlem4  20524  logtayllem  20538  logtayl  20539  cxpcl  20553  recxpcl  20554  leibpilem2  20769  leibpi  20770  rlimcnp2  20793  efrlim  20796  pclogsum  20987  dchrelbasd  21011  lgsfcl2  21074  lgscllem  21075  lgsval2lem  21078  lgsne0  21105  dchrvmasumiflem1  21183  dchrvmasumiflem2  21184  dchrisum0flblem1  21190  pntrlog2bndlem4  21262  pntrlog2bndlem5  21263  pntlemj  21285  padicabv  21312  xrge0iifcnv  24307  xrge0iifhom  24311  pnfneige0  24324  esumpinfval  24451  sigaclfu2  24492  ballotlemsv  24755  ballotlemsdom  24757  igamf  24823  igamcl  24824  itg2addnclem2  26203  itg2gt0cn  26206  ibladdnclem  26207  itgaddnclem1  26209  iblabsnclem  26214  iblabsnc  26215  iblmulc2nc  26216  itgmulc2nclem1  26217  bddiblnc  26221  itggt0cn  26223  areacirc  26234  pmtrf  27312  sdrgacs  27424  climsuse  27648  cdleme27cl  31002
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 2416
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 2422  df-cleq 2428  df-clel 2431  df-if 3732
  Copyright terms: Public domain W3C validator