Theorem iffalse 4095

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.

Step	Hyp	Ref	Expression
1		dedlemb 1003	. . 3 |- ( -. ph -> ( x e. B <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
2	1	abbi2dv 2742	. 2 |- ( -. ph -> B = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
3		df-if 4087	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
4	2, 3	syl6reqr 2675	1 |- ( -. ph -> if ( ph , A , B ) = B )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   {cab 2608   ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  iffalsei  4096  iffalsed  4097  ifnefalse  4098  ifsb  4099  ifbi  4107  ifeq1da  4116  ifeq12da  4118  ifclda  4120  ifeqda  4121  elimif  4122  ifbothda  4123  ifid  4125  ifnot  4133  ifan  4134  ifor  4135  2if2  4136  ifcomnan  4137  elimhyp  4146  elimhyp2v  4147  elimhyp3v  4148  elimhyp4v  4149  elimdhyp  4151  keephyp2v  4153  keephyp3v  4154  dfopif  4399  opprc  4424  somin1  5529  dfiota4OLD  5880  elimdelov  6736  ovif12  6739  oevn0  7595  pw2f1olem  8064  unxpdomlem2  8165  unxpdomlem3  8166  oi0  8433  wemaplem2  8452  ixpiunwdom  8496  cantnfp1lem3  8577  cantnflem1  8586  dfac12lem2  8966  fin23lem14  9155  axcc2lem  9258  ttukeylem5  9335  uzin  11720  xrmax1  12006  xrmax2  12007  xrmin1  12008  xrmin2  12009  max1ALT  12017  ifle  12028  xmulneg1  12099  modifeq2int  12732  seqf1olem1  12840  seqf1olem2  12841  bcval3  13093  swrdccat  13493  swrdccat3a  13494  swrdccat3b  13496  repswswrd  13531  cshword  13537  ccatco  13581  sumrblem  14442  fsumcvg  14443  summolem2a  14446  sumss  14455  fsumcvg2  14458  sumsplit  14499  prodeq2ii  14643  prodrblem  14659  fprodcvg  14660  prodmolem2a  14664  zprod  14667  prodss  14677  ruclem2  14961  ruclem3  14962  flodddiv4  15137  sadadd2lem2  15172  sadcp1  15177  sadcaddlem  15179  gcdn0val  15220  dfgcd2  15263  lcmn0val  15308  lcmfn0val  15336  pcgcd  15582  pcmptcl  15595  pcmpt  15596  pcmpt2  15597  pcprod  15599  fldivp1  15601  prmreclem2  15621  prmreclem4  15623  vdwlem6  15690  prmo1  15741  prmop1  15742  fvprmselelfz  15748  fvprmselgcd1  15749  ressval2  15929  xpsaddlem  16235  xpsvsca  16239  mreexexd  16308  setcepi  16738  pmtrmvd  17876  mvrf1  19425  mplcoe3  19466  mplmon2  19493  psrbagsn  19495  evlslem1  19515  obselocv  20072  dmatmul  20303  1mavmul  20354  mulmarep1gsum2  20380  1marepvmarrepid  20381  mdetdiag  20405  mdetrsca2  20410  mdetrlin2  20413  mdetunilem5  20422  mdetunilem7  20424  mdetunilem8  20425  mdetunilem9  20426  mndifsplit  20442  maducoeval2  20446  madugsum  20449  madurid  20450  smadiadetglem2  20478  1elcpmat  20520  decpmatid  20575  ptpjpre1  21374  ptbasfi  21384  isfcls  21813  ptcmplem2  21857  ptcmplem3  21858  dscmet  22377  dscopn  22378  icccmplem2  22626  cnmpt2pc  22727  iccpnfcnv  22743  xrhmeo  22745  pcoval2  22816  pcohtpylem  22819  pcopt  22822  pcopt2  22823  pcoass  22824  pcorevlem  22826  i1f1lem  23456  itg1addlem2  23464  itg1addlem3  23465  i1fres  23472  itg1climres  23481  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  itg2const2  23508  itg2seq  23509  itg2uba  23510  itg2splitlem  23515  itg2split  23516  itg2monolem1  23517  itg2gt0  23527  itg2cnlem1  23528  itg2cnlem2  23529  iblss  23571  iblss2  23572  itgle  23576  itgss  23578  ibladdlem  23586  itgaddlem1  23589  iblabslem  23594  iblabs  23595  iblabsr  23596  iblmulc2  23597  bddmulibl  23605  ditgneg  23621  elply2  23952  coeeq2  23998  dgrle  23999  coe1termlem  24014  logcnlem3  24390  igamgam  24775  isppw  24840  isnsqf  24861  mule1  24874  sqff1o  24908  chtublem  24936  dchrelbasd  24964  bposlem1  25009  bposlem3  25011  bposlem5  25013  bposlem6  25014  lgsneg  25046  lgsdilem  25049  lgsdir2  25055  lgsdir  25057  lgsdi  25059  lgsne0  25060  gausslemma2dlem1a  25090  2lgslem1c  25118  2lgs  25132  dchrvmasum2if  25186  ostth2lem4  25325  axlowdimlem15  25836  elimifd  29362  elim2if  29363  ifeq3da  29365  imadifxp  29414  resvval2  29829  pmtridf1o  29856  xrge0iifcnv  29979  indval2  30076  ddeval0  30298  eulerpartlemb  30430  plymulx0  30624  signsw0glem  30630  signswmnd  30634  dfrdg2  31701  dfrdg3  31702  noprefixmo  31848  nosupno  31849  nosupdm  31850  nosupbday  31851  nosupfv  31852  nosupres  31853  nosupbnd1lem1  31854  unisnif  32032  dfrdg4  32058  bj-xpima1sn  32943  finxpreclem2  33227  finxpreclem5  33232  matunitlindflem1  33405  poimirlem15  33424  poimirlem23  33432  mbfposadd  33457  itg2addnclem  33461  itg2addnclem3  33463  itg2gt0cn  33465  ibladdnclem  33466  itgaddnclem1  33468  iblabsnclem  33473  iblabsnc  33474  iblmulc2nc  33475  bddiblnc  33480  ftc1anclem5  33489  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  areacirclem5  33504  areacirc  33505  heiborlem4  33613  ac6s6  33980  riotaclbgBAD  34240  cdleme27a  35655  cdleme31sn2  35677  dihvalc  36522  mapdhval2  37015  hdmap1val2  37090  pw2f1ocnv  37604  aomclem5  37628  arearect  37801  areaquad  37802  upbdrech2  39522  lptioo2  39863  lptioo1  39864  limsupmnfuzlem  39958  limsupre3uzlem  39967  limsup10exlem  40004  coskpi2  40077  cosknegpi  40080  icccncfext  40100  cncfiooicclem1  40106  cncfiooiccre  40108  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  itgioocnicc  40193  iblcncfioo  40194  volico  40200  sublevolico  40201  voliooico  40209  voliccico  40216  dirkerper  40313  dirkertrigeq  40318  dirkercncflem2  40321  fourierdlem10  40334  fourierdlem32  40356  fourierdlem33  40357  fourierdlem37  40361  fourierdlem62  40385  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem79  40402  fourierdlem81  40404  fourierdlem82  40405  fourierdlem93  40416  fourierdlem97  40420  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  sqwvfoura  40445  sqwvfourb  40446  fourierswlem  40447  fouriersw  40448  elaa2lem  40450  etransclem15  40466  etransclem19  40470  etransclem23  40474  etransclem24  40475  etransclem25  40476  ioorrnopnxrlem  40526  nnfoctbdjlem  40672  isomenndlem  40744  ovn0  40780  hsphoidmvle2  40799  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmv1le  40808  hoidmvlelem2  40810  hoidmvlelem3  40811  ovnhoilem1  40815  hspdifhsp  40830  hoidifhspdmvle  40834  hspmbllem1  40840  hspmbllem2  40841  hspmbl  40843  volico2  40855  ovolval4lem2  40864  ovolval5lem1  40866  afvnfundmuv  41219  pfxccat3a  41429  cshword2  41437  suppmptcfin  42160  linc1  42214  ifnmfalse  42504