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

Theorem ifclda 3818
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 3794 . . . 4  |-  ( ps 
->  if ( ps ,  A ,  B )  =  A )
21adantl 463 . . 3  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  =  A )
3 ifclda.1 . . 3  |-  ( (
ph  /\  ps )  ->  A  e.  C )
42, 3eqeltrd 2515 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  e.  C )
5 iffalse 3796 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  A ,  B
)  =  B )
65adantl 463 . . 3  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  =  B )
7 ifclda.2 . . 3  |-  ( (
ph  /\  -.  ps )  ->  B  e.  C )
86, 7eqeltrd 2515 . 2  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  e.  C )
94, 8pm2.61dan 784 1  |-  ( ph  ->  if ( ps ,  A ,  B )  e.  C )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    = wceq 1364    e. wcel 1761   ifcif 3788
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-if 3789
This theorem is referenced by:  unxpdomlem3  7515  acndom  8217  iunfictbso  8280  dfac12lem2  8309  ttukeylem6  8679  canthp1lem2  8816  xaddf  11190  xmulf  11231  ccatcl  12270  swrdcl  12311  ccatco  12459  lo1bdd2  12998  o1lo1  13011  sadadd2lem2  13642  sadcaddlem  13649  sadadd2lem  13651  sadadd3  13653  iserodd  13898  prmreclem2  13974  prmreclem4  13976  prmreclem6  13978  prmrec  13979  vdwlem6  14043  symgextf  15915  pmtrf  15954  cyggex2  16366  dprdfid  16497  dprdfidOLD  16504  dmdprdsplitlem  16524  dmdprdsplitlemOLD  16525  cygznlem1  17958  cygznlem2a  17959  cygznlem3  17961  cygth  17963  ptpjpre2  19112  ptopn2  19116  ptpjopn  19144  iccpnfcnv  20475  xrhmeo  20477  cmetcaulem  20758  ovolunlem1a  20938  ovolunlem1  20939  ioorf  21012  mbfi1fseqlem3  21154  mbfi1flim  21160  itg2seq  21179  itg2splitlem  21185  itg2split  21186  iblss  21241  itgle  21246  itgeqa  21250  ibladdlem  21256  itgaddlem1  21259  iblabslem  21264  iblabs  21265  iblabsr  21266  iblmulc2  21267  itgmulc2lem1  21268  bddmulibl  21275  itggt0  21278  itgcn  21279  ellimc2  21311  limccnp  21325  limccnp2  21326  dvcobr  21379  lhop1  21445  elplyd  21629  coeeq2  21669  dvply1  21709  aalioulem3  21759  dvtaylp  21794  dvradcnv  21845  psercnlem1  21849  logcnlem2  22047  logcnlem3  22048  logcnlem4  22049  logtayllem  22063  logtayl  22064  cxpcl  22078  recxpcl  22079  leibpilem2  22295  leibpi  22296  rlimcnp2  22319  efrlim  22322  pclogsum  22513  dchrelbasd  22537  lgsfcl2  22600  lgscllem  22601  lgsval2lem  22604  lgsne0  22631  dchrvmasumiflem1  22709  dchrvmasumiflem2  22710  dchrisum0flblem1  22716  pntrlog2bndlem4  22788  pntrlog2bndlem5  22789  pntlemj  22811  padicabv  22838  sgnsval  26124  xrge0iifcnv  26299  xrge0iifhom  26303  pnfneige0  26317  esumpinfval  26458  sigaclfu2  26500  ballotlemsv  26822  ballotlemsdom  26824  signsvvf  26910  signsvfn  26913  igamf  26967  igamcl  26968  itg2addnclem2  28369  itg2gt0cn  28372  ibladdnclem  28373  itgaddnclem1  28375  iblabsnclem  28380  iblabsnc  28381  iblmulc2nc  28382  itgmulc2nclem1  28383  bddiblnc  28387  itggt0cn  28389  ftc1anclem5  28396  ftc1anclem6  28397  ftc1anclem7  28398  ftc1anclem8  28399  ftc1anc  28400  areacirc  28414  sdrgacs  29483  climsuse  29706  lincext1  30829  cdleme27cl  33732
  Copyright terms: Public domain W3C validator