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

Theorem iffalse 3748
Description: Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.)
Assertion
Ref Expression
iffalse  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )

Proof of Theorem iffalse
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 dedlemb 923 . . 3  |-  ( -. 
ph  ->  ( x  e.  B  <->  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) ) )
21abbi2dv 2553 . 2  |-  ( -. 
ph  ->  B  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) } )
3 df-if 3742 . 2  |-  if (
ph ,  A ,  B )  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) }
42, 3syl6reqr 2489 1  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 359    /\ wa 360    = wceq 1653    e. wcel 1726   {cab 2424   ifcif 3741
This theorem is referenced by:  ifnefalse  3749  ifsb  3750  ifbi  3758  ifeq1da  3766  ifclda  3768  elimif  3770  ifbothda  3771  ifid  3773  ifeqor  3778  ifnot  3779  ifan  3780  ifor  3781  elimhyp  3789  elimhyp2v  3790  elimhyp3v  3791  elimhyp4v  3792  elimdhyp  3794  keephyp2v  3796  keephyp3v  3797  dfopif  3983  opprc  4007  somin1  5273  somincom  5274  dfiota4  5449  elimdelov  6156  riotav  6557  riotaund  6589  tz7.44-2  6668  tz7.44-3  6669  oevn0  6762  pw2f1olem  7215  unxpdomlem2  7317  unxpdomlem3  7318  oi0  7500  wemaplem2  7519  unwdomg  7555  ixpiunwdom  7562  cantnfp1lem1  7637  cantnfp1lem3  7639  cantnflem1d  7647  cantnflem1  7648  dfac12lem2  8029  fin23lem14  8218  axcc2lem  8321  ttukeylem5  8398  ttukeylem7  8400  canthp1lem2  8533  pwfseqlem3  8540  uzin  10523  xrmax1  10768  xrmax2  10769  xrmin1  10770  xrmin2  10771  max1ALT  10779  ifle  10788  xmulneg1  10853  rexmul  10855  xmulpnf1  10858  fzprval  11111  seqf1olem1  11367  seqf1olem2  11368  expnnval  11390  expneg  11394  bcval3  11602  ccatval2  11751  ccatco  11809  absmax  12138  sumeq2ii  12492  sumrblem  12510  fsumcvg  12511  summolem2a  12514  zsum  12517  sum0  12520  sumss  12523  sumss2  12525  fsumcvg2  12526  fsumsplit  12538  sumsplit  12557  ef0lem  12686  rpnnen2lem9  12827  ruclem2  12836  ruclem3  12837  sadadd2lem2  12967  sadcp1  12972  sadcaddlem  12974  sadadd2  12977  gcdn0val  13015  eucalgf  13079  eucalginv  13080  eucalglt  13081  iserodd  13214  pcgcd  13256  pcmptcl  13265  pcmpt  13266  pcmpt2  13267  pcprod  13269  fldivp1  13271  prmreclem2  13290  prmreclem4  13292  vdwlem6  13359  ramtub  13385  ressval2  13523  xpsaddlem  13805  xpsvsca  13809  setcepi  14248  gsumval2a  14787  mulgnn  14901  mulgnegnn  14905  odlem2  15182  dfod2  15205  gsumval3a  15517  gsumzsplit  15534  dmdprdsplitlem  15600  abvtrivd  15933  psrlidm  16472  psrridm  16473  mvridlem  16488  mvrf1  16494  mvrcl  16517  mplmon  16531  mplmonmul  16532  mplcoe1  16533  mplcoe3  16534  mplcoe2  16535  mplmon2  16558  psrbagsn  16560  coe1tmfv2  16672  obselocv  16960  ptpjpre1  17608  ptpjpre2  17617  ptbasfi  17618  ptopn2  17621  xkopt  17692  isfcls  18046  ptcmplem2  18089  ptcmplem3  18090  tsmssplit  18186  dscmet  18625  dscopn  18626  xrsxmet  18845  icccmplem2  18859  cnmpt2pc  18958  iccpnfcnv  18974  xrhmeo  18976  htpycc  19010  pco1  19045  pcoval2  19046  pcohtpylem  19049  pcopt  19052  pcopt2  19053  pcoass  19054  pcorevlem  19056  ovolunlem1a  19397  ovolunlem1  19398  ovolicc1  19417  i1f1lem  19584  itg11  19586  itg1addlem2  19592  itg1addlem3  19593  i1fres  19600  itg1climres  19609  mbfi1fseqlem4  19613  mbfi1fseqlem5  19614  mbfi1flim  19618  itg2const2  19636  itg2seq  19637  itg2uba  19638  itg2splitlem  19643  itg2split  19644  itg2monolem1  19645  itg2gt0  19655  itg2cnlem1  19656  itg2cnlem2  19657  itgeq2  19672  itg0  19674  iblss  19699  iblss2  19700  itgle  19704  itgss  19706  itgss2  19707  itgss3  19709  itgless  19711  ibladdlem  19714  itgaddlem1  19717  iblabslem  19722  iblabs  19723  iblabsr  19724  iblmulc2  19725  bddmulibl  19733  itggt0  19736  itgcn  19737  ditgneg  19749  limccnp2  19784  dvexp2  19845  lhop2  19904  evlslem3  19940  evlslem1  19941  deg1add  20031  ig1pval3  20102  elply2  20120  ply1termlem  20127  plyeq0lem  20134  plypf1  20136  coeeq2  20166  dgrle  20167  coe1termlem  20181  dvply1  20206  vieta1lem2  20233  pserdvlem2  20349  abelthlem9  20361  logcnlem3  20540  logtayllem  20555  logtayl  20556  cxpef  20561  rlimcnp2  20810  efrlim  20813  isppw  20902  isnsqf  20923  mule1  20936  sqff1o  20970  muinv  20983  chtublem  21000  dchrelbasd  21028  bposlem1  21073  bposlem3  21075  bposlem5  21077  bposlem6  21078  lgsval2lem  21095  lgsval4  21105  lgsval4a  21107  lgsneg  21108  lgsneg1  21109  lgsdilem  21111  lgsdir2  21117  lgsdir  21119  lgsdi  21121  lgsne0  21122  rplogsumlem2  21184  dchrvmasum2if  21196  dchrisum0fno1  21210  rplogsum  21226  pntrlog2bndlem4  21279  pntrlog2bndlem5  21280  padicabv  21329  ostth1  21332  ostth2lem4  21335  ostth3  21337  gxpval  21852  gxnval  21853  ifbieq12d2  24007  elimifd  24009  elim2if  24010  imadifxp  24043  partfun  24092  xrge0iifcnv  24324  xrge0iifcv  24325  xrge0iif1  24329  indval2  24417  ind0  24422  esumpinfval  24468  sigaclfu2  24509  ballotlemrv2  24784  igamgam  24838  prodeq2ii  25244  prodrblem  25260  fprodcvg  25261  prodmolem2a  25265  zprod  25268  fprodntriv  25273  prod0  25274  prodss  25278  fprodsplit  25294  dfrdg2  25428  dfrdg3  25429  unisnif  25775  dfrdg4  25800  axlowdimlem15  25900  axlowdim  25905  mblfinlem2  26256  mbfposadd  26266  itg2addnclem  26270  itg2addnclem2  26271  itg2addnclem3  26272  itg2gt0cn  26274  ibladdnclem  26275  itgaddnclem1  26277  iblabsnclem  26282  iblabsnc  26283  iblmulc2nc  26284  bddiblnc  26289  ftc1anclem5  26298  ftc1anclem6  26299  ftc1anclem7  26300  ftc1anclem8  26301  ftc1anc  26302  areacirclem5  26310  areacirc  26311  fdc  26463  heiborlem4  26537  heiborlem6  26539  pw2f1ocnv  27122  aomclem5  27147  kelac1  27152  uvcvv0  27230  uvcff  27231  flcidc  27370  pmtrmvd  27389  mamulid  27449  mamurid  27450  refsum2cnlem1  27698  afvnfundmuv  27993  ifeqda  28066  2if2  28067  modifeq2int  28184  swrdnd  28216  swrd0  28217  swrdvalodm2  28222  swrdvalodm  28223  swrdccatin2  28244  swrdccat  28250  swrdccat3a  28251  swrdccat3b  28253  cshwidxm  28280  cshwidxn  28281  2cshw  28290  2cshwcom  28301  ifnmfalse  28580  sgnp  28594  sgnn  28598  cdleme27a  31238  cdleme31sn2  31260  cdleme31fv2  31264  cdlemefr27cl  31274  dihvalc  32105  mapdhval2  32598  hdmap1val2  32673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-if 3742
  Copyright terms: Public domain W3C validator