Theorem iffalse 3794

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 946	. . 3 |- ( -. ph -> ( x e. B <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
2	1	abbi2dv 2553	. 2 |- ( -. ph -> B = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
3		df-if 3787	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
4	2, 3	syl6reqr 2489	1 |- ( -. ph -> if ( ph , A , B ) = B )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 368   /\ wa 369   = wceq 1369   e. wcel 1756   {cab 2424   ifcif 3786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-if 3787

This theorem is referenced by:  iffalsei  3795  ifnefalse  3796  ifsb  3797  ifbi  3805  ifeq1da  3814  ifclda  3816  ifeqda  3817  elimif  3818  ifbothda  3819  ifid  3821  ifeqor  3828  ifnot  3829  ifan  3830  ifor  3831  2if2  3832  ifcomnan  3833  elimhyp  3843  elimhyp2v  3844  elimhyp3v  3845  elimhyp4v  3846  elimdhyp  3848  keephyp2v  3850  keephyp3v  3851  dfopif  4051  opprc  4076  somin1  5229  somincom  5230  dfiota4  5404  elimdelov  6162  ovif12  6165  mpt2difsnif  6178  tz7.44-2  6855  tz7.44-3  6856  oevn0  6947  pw2f1olem  7407  unxpdomlem2  7510  unxpdomlem3  7511  sniffsupp  7651  oi0  7734  wemaplem2  7753  unwdomg  7791  ixpiunwdom  7798  cantnfp1lem1  7878  cantnfp1lem3  7880  cantnflem1d  7888  cantnflem1  7889  cantnfp1lem1OLD  7904  cantnfp1lem3OLD  7906  cantnflem1dOLD  7911  cantnflem1OLD  7912  dfac12lem2  8305  fin23lem14  8494  axcc2lem  8597  ttukeylem5  8674  ttukeylem7  8676  canthp1lem2  8812  pwfseqlem3  8819  uzin  10885  xrmax1  11139  xrmax2  11140  xrmin1  11141  xrmin2  11142  max1ALT  11150  ifle  11159  xmulneg1  11224  rexmul  11226  xmulpnf1  11229  fzprval  11509  modifeq2int  11753  seqf1olem1  11837  seqf1olem2  11838  expnnval  11860  expneg  11865  bcval3  12074  ccatval2  12269  lswccatn0lsw  12279  swrdnd  12318  swrd0  12319  swrdvalodm2  12325  swrdvalodm  12326  swrdccatin2  12370  swrdccat  12376  swrdccat3a  12377  swrdccat3b  12379  repswswrd  12414  cshword  12420  ccatco  12455  sgnp  12571  sgnn  12575  absmax  12809  sumeq2ii  13162  sumrblem  13180  fsumcvg  13181  summolem2a  13184  sumss  13193  sumss2  13195  fsumcvg2  13196  fsumsplit  13208  sumsplit  13227  ef0lem  13356  rpnnen2lem9  13497  ruclem2  13506  ruclem3  13507  sadadd2lem2  13638  sadcp1  13643  sadcaddlem  13645  sadadd2  13648  gcdn0val  13686  eucalgf  13750  eucalginv  13751  eucalglt  13752  iserodd  13894  pcgcd  13936  pcmptcl  13945  pcmpt  13946  pcmpt2  13947  pcprod  13949  fldivp1  13951  prmreclem2  13970  prmreclem4  13972  vdwlem6  14039  ramtub  14065  ressval2  14219  xpsaddlem  14505  xpsvsca  14509  setcepi  14948  gsumval2a  15503  mulgnn  15624  mulgnegnn  15628  symgextfv  15914  pmtrprfv3  15951  pmtrmvd  15953  pmtrdifellem4  15976  pmtrprfval  15984  pmtrprfvalrn  15985  odlem2  16033  dfod2  16056  gsumval3a  16370  gsumval3aOLD  16371  gsumzsplit  16409  gsumzsplitOLD  16410  dmdprdsplitlem  16524  dmdprdsplitlemOLD  16525  abvtrivd  16905  psrlidm  17454  psrlidmOLD  17455  psrridm  17456  psrridmOLD  17457  mvridlemOLD  17472  mvrf1  17478  mvrcl  17508  mplmon  17522  mplmonmul  17523  mplcoe1  17524  mplcoe3  17525  mplcoe3OLD  17526  mplcoe5  17528  mplcoe2OLD  17530  mplmon2  17555  psrbagsn  17557  evlslem3  17580  evlslem1  17581  coe1tmfv2  17708  obselocv  18133  uvcvv0  18195  uvcff  18196  1mavmul  18339  mulmarep1gsum1  18364  mulmarep1gsum2  18365  1marepvmarrepid  18366  1marepvsma1  18374  mdet1  18388  mdetrsca2  18391  mdetrlin2  18393  mdetunilem2  18399  mdetunilem5  18402  mdetunilem7  18404  mdetunilem8  18405  mdetunilem9  18406  mndifsplit  18422  maducoeval2  18426  madugsum  18429  madurid  18430  symgmatr01lem  18439  gsummatr01lem3  18443  gsummatr01lem4  18444  gsummatr01  18445  smadiadetglem2  18458  ptpjpre1  19124  ptpjpre2  19133  ptbasfi  19134  ptopn2  19137  xkopt  19208  isfcls  19562  ptcmplem2  19605  ptcmplem3  19606  tsmssplit  19706  dscmet  20145  dscopn  20146  xrsxmet  20366  icccmplem2  20380  cnmpt2pc  20480  iccpnfcnv  20496  xrhmeo  20498  htpycc  20532  pco1  20567  pcoval2  20568  pcohtpylem  20571  pcopt  20574  pcopt2  20575  pcoass  20576  pcorevlem  20578  ovolunlem1a  20959  ovolunlem1  20960  ovolicc1  20979  i1f1lem  21147  itg11  21149  itg1addlem2  21155  itg1addlem3  21156  i1fres  21163  itg1climres  21172  mbfi1fseqlem4  21176  mbfi1fseqlem5  21177  mbfi1flim  21181  itg2const2  21199  itg2seq  21200  itg2uba  21201  itg2splitlem  21206  itg2split  21207  itg2monolem1  21208  itg2gt0  21218  itg2cnlem1  21219  itg2cnlem2  21220  itgeq2  21235  iblss  21262  iblss2  21263  itgle  21267  itgss  21269  itgss2  21270  itgss3  21272  itgless  21274  ibladdlem  21277  itgaddlem1  21280  iblabslem  21285  iblabs  21286  iblabsr  21287  iblmulc2  21288  bddmulibl  21296  itggt0  21299  itgcn  21300  ditgneg  21312  limccnp2  21347  dvexp2  21408  lhop2  21467  deg1add  21555  ig1pval3  21626  elply2  21644  ply1termlem  21651  plyeq0lem  21658  plypf1  21660  coeeq2  21690  dgrle  21691  coe1termlem  21705  dvply1  21730  pserdvlem2  21873  abelthlem9  21885  logcnlem3  22069  logtayllem  22084  logtayl  22085  cxpef  22090  rlimcnp2  22340  efrlim  22343  isppw  22432  isnsqf  22453  mule1  22466  sqff1o  22500  muinv  22513  chtublem  22530  dchrelbasd  22558  bposlem1  22603  bposlem3  22605  bposlem5  22607  bposlem6  22608  lgsval2lem  22625  lgsval4  22635  lgsval4a  22637  lgsneg  22638  lgsneg1  22639  lgsdilem  22641  lgsdir2  22647  lgsdir  22649  lgsdi  22651  lgsne0  22652  rplogsumlem2  22714  dchrvmasum2if  22726  dchrisum0fno1  22740  rplogsum  22756  pntrlog2bndlem4  22809  pntrlog2bndlem5  22810  padicabv  22859  ostth1  22862  ostth2lem4  22865  ostth3  22867  axlowdimlem15  23170  axlowdim  23175  gxpval  23714  gxnval  23715  ifbieq12d2  25871  elimifd  25873  elim2if  25874  imadifxp  25907  partfun  25961  resvval2  26266  xrge0iifcnv  26332  xrge0iifcv  26333  xrge0iif1  26337  indval2  26440  ind0  26445  esumpinfval  26491  sigaclfu2  26533  ddeval0  26620  eulerpartlemb  26720  eulerpartlemgs2  26732  ballotlemrv2  26873  plymulx0  26917  signsw0glem  26923  signswmnd  26927  signswlid  26929  signsvtp  26953  signlem0  26957  igamgam  27004  prodeq2ii  27395  prodrblem  27411  fprodcvg  27412  prodmolem2a  27416  zprod  27419  fprodntriv  27424  prodss  27429  fprodsplit  27445  dfrdg2  27578  dfrdg3  27579  unisnif  27925  dfrdg4  27950  mblfinlem2  28400  mbfposadd  28410  itg2addnclem  28414  itg2addnclem2  28415  itg2addnclem3  28416  itg2gt0cn  28418  ibladdnclem  28419  itgaddnclem1  28421  iblabsnclem  28426  iblabsnc  28427  iblmulc2nc  28428  bddiblnc  28433  ftc1anclem5  28442  ftc1anclem6  28443  ftc1anclem7  28444  ftc1anclem8  28445  ftc1anc  28446  areacirclem5  28459  areacirc  28460  fdc  28612  heiborlem4  28684  heiborlem6  28686  ac6s6  28955  pw2f1ocnv  29357  aomclem5  29382  kelac1  29387  flcidc  29502  arearect  29562  areaquad  29563  refsum2cnlem1  29730  afvnfundmuv  30016  clwlkisclwwlklem2fv2  30416  fdmdifeqresdif  30702  suppmptcfin  30762  gsummoncoe1  30808  dmatmul  30836  scmatsubcl  30844  scmatmulcl  30846  mdetdiag  30867  linc1  30890  ifnmfalse  31029  bj-xpima1sn  32348  riotaclbgBAD  32498  riotaclbBAD  32499  cdleme27a  33904  cdleme31sn2  33926  cdleme31fv2  33930  cdlemefr27cl  33940  dihvalc  34771  mapdhval2  35264  hdmap1val2  35339