Theorem iffalse 3787

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 939	. . 3 |- ( -. ph -> ( x e. B <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
2	1	abbi2dv 2548	. 2 |- ( -. ph -> B = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
3		df-if 3780	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
4	2, 3	syl6reqr 2484	1 |- ( -. ph -> if ( ph , A , B ) = B )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 368   /\ wa 369   = wceq 1362   e. wcel 1755   {cab 2419   ifcif 3779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-if 3780

This theorem is referenced by:  iffalsei  3788  ifnefalse  3789  ifsb  3790  ifbi  3798  ifeq1da  3807  ifclda  3809  ifeqda  3810  elimif  3811  ifbothda  3812  ifid  3814  ifeqor  3821  ifnot  3822  ifan  3823  ifor  3824  2if2  3825  ifcomnan  3826  elimhyp  3836  elimhyp2v  3837  elimhyp3v  3838  elimhyp4v  3839  elimdhyp  3841  keephyp2v  3843  keephyp3v  3844  dfopif  4044  opprc  4069  somin1  5222  somincom  5223  dfiota4  5397  elimdelov  6156  ovif12  6159  mpt2difsnif  6172  tz7.44-2  6849  tz7.44-3  6850  oevn0  6943  pw2f1olem  7403  unxpdomlem2  7506  unxpdomlem3  7507  sniffsupp  7647  oi0  7730  wemaplem2  7749  unwdomg  7787  ixpiunwdom  7794  cantnfp1lem1  7874  cantnfp1lem3  7876  cantnflem1d  7884  cantnflem1  7885  cantnfp1lem1OLD  7900  cantnfp1lem3OLD  7902  cantnflem1dOLD  7907  cantnflem1OLD  7908  dfac12lem2  8301  fin23lem14  8490  axcc2lem  8593  ttukeylem5  8670  ttukeylem7  8672  canthp1lem2  8807  pwfseqlem3  8814  uzin  10880  xrmax1  11134  xrmax2  11135  xrmin1  11136  xrmin2  11137  max1ALT  11145  ifle  11154  xmulneg1  11219  rexmul  11221  xmulpnf1  11224  fzprval  11500  modifeq2int  11744  seqf1olem1  11828  seqf1olem2  11829  expnnval  11851  expneg  11856  bcval3  12065  ccatval2  12260  lswccatn0lsw  12270  swrdnd  12309  swrd0  12310  swrdvalodm2  12316  swrdvalodm  12317  swrdccatin2  12361  swrdccat  12367  swrdccat3a  12368  swrdccat3b  12370  repswswrd  12405  cshword  12411  ccatco  12446  sgnp  12562  sgnn  12566  absmax  12800  sumeq2ii  13153  sumrblem  13171  fsumcvg  13172  summolem2a  13175  sumss  13184  sumss2  13186  fsumcvg2  13187  fsumsplit  13199  sumsplit  13218  ef0lem  13346  rpnnen2lem9  13487  ruclem2  13496  ruclem3  13497  sadadd2lem2  13628  sadcp1  13633  sadcaddlem  13635  sadadd2  13638  gcdn0val  13676  eucalgf  13740  eucalginv  13741  eucalglt  13742  iserodd  13884  pcgcd  13926  pcmptcl  13935  pcmpt  13936  pcmpt2  13937  pcprod  13939  fldivp1  13941  prmreclem2  13960  prmreclem4  13962  vdwlem6  14029  ramtub  14055  ressval2  14209  xpsaddlem  14495  xpsvsca  14499  setcepi  14938  gsumval2a  15491  mulgnn  15612  mulgnegnn  15616  symgextfv  15902  pmtrprfv3  15939  pmtrmvd  15941  pmtrdifellem4  15964  pmtrprfval  15972  pmtrprfvalrn  15973  odlem2  16021  dfod2  16044  gsumval3a  16358  gsumval3aOLD  16359  gsumzsplit  16397  gsumzsplitOLD  16398  dmdprdsplitlem  16507  dmdprdsplitlemOLD  16508  abvtrivd  16848  psrlidm  17407  psrlidmOLD  17408  psrridm  17409  psrridmOLD  17410  mvridlemOLD  17425  mvrf1  17431  mvrcl  17461  mplmon  17475  mplmonmul  17476  mplcoe1  17477  mplcoe3  17478  mplcoe3OLD  17479  mplcoe2  17480  mplcoe2OLD  17481  mplmon2  17506  psrbagsn  17508  coe1tmfv2  17625  obselocv  17994  uvcvv0  18056  uvcff  18057  1mavmul  18200  mulmarep1gsum1  18225  mulmarep1gsum2  18226  1marepvmarrepid  18227  1marepvsma1  18235  mdet1  18249  mdetrsca2  18252  mdetrlin2  18254  mdetunilem2  18260  mdetunilem5  18263  mdetunilem7  18265  mdetunilem8  18266  mdetunilem9  18267  mndifsplit  18283  maducoeval2  18287  madugsum  18290  madurid  18291  symgmatr01lem  18300  gsummatr01lem3  18304  gsummatr01lem4  18305  gsummatr01  18306  smadiadetglem2  18319  ptpjpre1  18985  ptpjpre2  18994  ptbasfi  18995  ptopn2  18998  xkopt  19069  isfcls  19423  ptcmplem2  19466  ptcmplem3  19467  tsmssplit  19567  dscmet  20006  dscopn  20007  xrsxmet  20227  icccmplem2  20241  cnmpt2pc  20341  iccpnfcnv  20357  xrhmeo  20359  htpycc  20393  pco1  20428  pcoval2  20429  pcohtpylem  20432  pcopt  20435  pcopt2  20436  pcoass  20437  pcorevlem  20439  ovolunlem1a  20820  ovolunlem1  20821  ovolicc1  20840  i1f1lem  21008  itg11  21010  itg1addlem2  21016  itg1addlem3  21017  i1fres  21024  itg1climres  21033  mbfi1fseqlem4  21037  mbfi1fseqlem5  21038  mbfi1flim  21042  itg2const2  21060  itg2seq  21061  itg2uba  21062  itg2splitlem  21067  itg2split  21068  itg2monolem1  21069  itg2gt0  21079  itg2cnlem1  21080  itg2cnlem2  21081  itgeq2  21096  iblss  21123  iblss2  21124  itgle  21128  itgss  21130  itgss2  21131  itgss3  21133  itgless  21135  ibladdlem  21138  itgaddlem1  21141  iblabslem  21146  iblabs  21147  iblabsr  21148  iblmulc2  21149  bddmulibl  21157  itggt0  21160  itgcn  21161  ditgneg  21173  limccnp2  21208  dvexp2  21269  lhop2  21328  evlslem3  21365  evlslem1  21366  deg1add  21459  ig1pval3  21530  elply2  21548  ply1termlem  21555  plyeq0lem  21562  plypf1  21564  coeeq2  21594  dgrle  21595  coe1termlem  21609  dvply1  21634  pserdvlem2  21777  abelthlem9  21789  logcnlem3  21973  logtayllem  21988  logtayl  21989  cxpef  21994  rlimcnp2  22244  efrlim  22247  isppw  22336  isnsqf  22357  mule1  22370  sqff1o  22404  muinv  22417  chtublem  22434  dchrelbasd  22462  bposlem1  22507  bposlem3  22509  bposlem5  22511  bposlem6  22512  lgsval2lem  22529  lgsval4  22539  lgsval4a  22541  lgsneg  22542  lgsneg1  22543  lgsdilem  22545  lgsdir2  22551  lgsdir  22553  lgsdi  22555  lgsne0  22556  rplogsumlem2  22618  dchrvmasum2if  22630  dchrisum0fno1  22644  rplogsum  22660  pntrlog2bndlem4  22713  pntrlog2bndlem5  22714  padicabv  22763  ostth1  22766  ostth2lem4  22769  ostth3  22771  axlowdimlem15  23024  axlowdim  23029  gxpval  23568  gxnval  23569  ifbieq12d2  25726  elimifd  25728  elim2if  25729  imadifxp  25762  partfun  25816  resvval2  26150  xrge0iifcnv  26216  xrge0iifcv  26217  xrge0iif1  26221  indval2  26324  ind0  26329  esumpinfval  26375  sigaclfu2  26417  ddeval0  26504  eulerpartlemb  26598  eulerpartlemgs2  26610  ballotlemrv2  26751  plymulx0  26795  signsw0glem  26801  signswmnd  26805  signswlid  26807  signsvtp  26831  signlem0  26835  igamgam  26882  prodeq2ii  27272  prodrblem  27288  fprodcvg  27289  prodmolem2a  27293  zprod  27296  fprodntriv  27301  prodss  27306  fprodsplit  27322  dfrdg2  27455  dfrdg3  27456  unisnif  27802  dfrdg4  27827  mblfinlem2  28270  mbfposadd  28280  itg2addnclem  28284  itg2addnclem2  28285  itg2addnclem3  28286  itg2gt0cn  28288  ibladdnclem  28289  itgaddnclem1  28291  iblabsnclem  28296  iblabsnc  28297  iblmulc2nc  28298  bddiblnc  28303  ftc1anclem5  28312  ftc1anclem6  28313  ftc1anclem7  28314  ftc1anclem8  28315  ftc1anc  28316  areacirclem5  28329  areacirc  28330  fdc  28482  heiborlem4  28554  heiborlem6  28556  ac6s6  28826  pw2f1ocnv  29228  aomclem5  29253  kelac1  29258  flcidc  29373  arearect  29433  areaquad  29434  refsum2cnlem1  29601  afvnfundmuv  29888  clwlkisclwwlklem2fv2  30288  fdmdifeqresdif  30573  suppmptcfin  30620  linc1  30665  ifnmfalse  30804  bj-xpima1sn  32028  riotaclbgBAD  32175  riotaclbBAD  32176  cdleme27a  33581  cdleme31sn2  33603  cdleme31fv2  33607  cdlemefr27cl  33617  dihvalc  34448  mapdhval2  34941  hdmap1val2  35016