Theorem iffalse 3897

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 2588	. 2 |- ( -. ph -> B = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
3		df-if 3890	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
4	2, 3	syl6reqr 2511	1 |- ( -. ph -> if ( ph , A , B ) = B )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 368   /\ wa 369   = wceq 1370   e. wcel 1758   {cab 2436   ifcif 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-if 3890

This theorem is referenced by:  iffalsei  3898  ifnefalse  3899  ifsb  3900  ifbi  3908  ifeq1da  3917  ifclda  3919  ifeqda  3920  elimif  3921  ifbothda  3922  ifid  3924  ifeqor  3931  ifnot  3932  ifan  3933  ifor  3934  2if2  3935  ifcomnan  3936  elimhyp  3946  elimhyp2v  3947  elimhyp3v  3948  elimhyp4v  3949  elimdhyp  3951  keephyp2v  3953  keephyp3v  3954  dfopif  4154  opprc  4179  somin1  5332  somincom  5333  dfiota4  5507  elimdelov  6266  ovif12  6269  mpt2difsnif  6283  tz7.44-2  6963  tz7.44-3  6964  oevn0  7055  pw2f1olem  7515  unxpdomlem2  7619  unxpdomlem3  7620  sniffsupp  7760  oi0  7843  wemaplem2  7862  unwdomg  7900  ixpiunwdom  7907  cantnfp1lem1  7987  cantnfp1lem3  7989  cantnflem1d  7997  cantnflem1  7998  cantnfp1lem1OLD  8013  cantnfp1lem3OLD  8015  cantnflem1dOLD  8020  cantnflem1OLD  8021  dfac12lem2  8414  fin23lem14  8603  axcc2lem  8706  ttukeylem5  8783  ttukeylem7  8785  canthp1lem2  8921  pwfseqlem3  8928  uzin  10994  xrmax1  11248  xrmax2  11249  xrmin1  11250  xrmin2  11251  max1ALT  11259  ifle  11268  xmulneg1  11333  rexmul  11335  xmulpnf1  11338  fzprval  11618  modifeq2int  11862  seqf1olem1  11946  seqf1olem2  11947  expnnval  11969  expneg  11974  bcval3  12183  ccatval2  12379  lswccatn0lsw  12389  swrdnd  12428  swrd0  12429  swrdvalodm2  12435  swrdvalodm  12436  swrdccatin2  12480  swrdccat  12486  swrdccat3a  12487  swrdccat3b  12489  repswswrd  12524  cshword  12530  ccatco  12565  sgnp  12681  sgnn  12685  absmax  12919  sumeq2ii  13272  sumrblem  13290  fsumcvg  13291  summolem2a  13294  sumss  13303  sumss2  13305  fsumcvg2  13306  fsumsplit  13318  sumsplit  13337  ef0lem  13466  rpnnen2lem9  13607  ruclem2  13616  ruclem3  13617  sadadd2lem2  13748  sadcp1  13753  sadcaddlem  13755  sadadd2  13758  gcdn0val  13796  eucalgf  13860  eucalginv  13861  eucalglt  13862  iserodd  14004  pcgcd  14046  pcmptcl  14055  pcmpt  14056  pcmpt2  14057  pcprod  14059  fldivp1  14061  prmreclem2  14080  prmreclem4  14082  vdwlem6  14149  ramtub  14175  ressval2  14329  xpsaddlem  14615  xpsvsca  14619  setcepi  15058  gsumval2a  15614  mulgnn  15735  mulgnegnn  15739  symgextfv  16025  pmtrprfv3  16062  pmtrmvd  16064  pmtrdifellem4  16087  pmtrprfval  16095  pmtrprfvalrn  16096  odlem2  16146  dfod2  16169  gsumval3a  16483  gsumval3aOLD  16484  gsumzsplit  16522  gsumzsplitOLD  16523  dmdprdsplitlem  16639  dmdprdsplitlemOLD  16640  abvtrivd  17031  psrlidm  17580  psrlidmOLD  17581  psrridm  17582  psrridmOLD  17583  mvridlemOLD  17599  mvrf1  17605  mvrcl  17635  mplmon  17649  mplmonmul  17650  mplcoe1  17651  mplcoe3  17652  mplcoe3OLD  17653  mplcoe5  17655  mplcoe2OLD  17657  mplmon2  17682  psrbagsn  17684  evlslem3  17707  evlslem1  17708  coe1tmfv2  17836  obselocv  18262  uvcvv0  18324  uvcff  18325  1mavmul  18470  mulmarep1gsum1  18495  mulmarep1gsum2  18496  1marepvmarrepid  18497  1marepvsma1  18505  mdetdiag  18521  mdetrsca2  18526  mdetrlin2  18529  mdetunilem2  18535  mdetunilem5  18538  mdetunilem7  18540  mdetunilem8  18541  mdetunilem9  18542  mndifsplit  18558  maducoeval2  18562  madugsum  18565  madurid  18566  symgmatr01lem  18575  gsummatr01lem3  18579  gsummatr01lem4  18580  gsummatr01  18581  smadiadetglem2  18594  ptpjpre1  19260  ptpjpre2  19269  ptbasfi  19270  ptopn2  19273  xkopt  19344  isfcls  19698  ptcmplem2  19741  ptcmplem3  19742  tsmssplit  19842  dscmet  20281  dscopn  20282  xrsxmet  20502  icccmplem2  20516  cnmpt2pc  20616  iccpnfcnv  20632  xrhmeo  20634  htpycc  20668  pco1  20703  pcoval2  20704  pcohtpylem  20707  pcopt  20710  pcopt2  20711  pcoass  20712  pcorevlem  20714  ovolunlem1a  21095  ovolunlem1  21096  ovolicc1  21115  i1f1lem  21283  itg11  21285  itg1addlem2  21291  itg1addlem3  21292  i1fres  21299  itg1climres  21308  mbfi1fseqlem4  21312  mbfi1fseqlem5  21313  mbfi1flim  21317  itg2const2  21335  itg2seq  21336  itg2uba  21337  itg2splitlem  21342  itg2split  21343  itg2monolem1  21344  itg2gt0  21354  itg2cnlem1  21355  itg2cnlem2  21356  itgeq2  21371  iblss  21398  iblss2  21399  itgle  21403  itgss  21405  itgss2  21406  itgss3  21408  itgless  21410  ibladdlem  21413  itgaddlem1  21416  iblabslem  21421  iblabs  21422  iblabsr  21423  iblmulc2  21424  bddmulibl  21432  itggt0  21435  itgcn  21436  ditgneg  21448  limccnp2  21483  dvexp2  21544  lhop2  21603  deg1add  21691  ig1pval3  21762  elply2  21780  ply1termlem  21787  plyeq0lem  21794  plypf1  21796  coeeq2  21826  dgrle  21827  coe1termlem  21841  dvply1  21866  pserdvlem2  22009  abelthlem9  22021  logcnlem3  22205  logtayllem  22220  logtayl  22221  cxpef  22226  rlimcnp2  22476  efrlim  22479  isppw  22568  isnsqf  22589  mule1  22602  sqff1o  22636  muinv  22649  chtublem  22666  dchrelbasd  22694  bposlem1  22739  bposlem3  22741  bposlem5  22743  bposlem6  22744  lgsval2lem  22761  lgsval4  22771  lgsval4a  22773  lgsneg  22774  lgsneg1  22775  lgsdilem  22777  lgsdir2  22783  lgsdir  22785  lgsdi  22787  lgsne0  22788  rplogsumlem2  22850  dchrvmasum2if  22862  dchrisum0fno1  22876  rplogsum  22892  pntrlog2bndlem4  22945  pntrlog2bndlem5  22946  padicabv  22995  ostth1  22998  ostth2lem4  23001  ostth3  23003  axlowdimlem15  23337  axlowdim  23342  gxpval  23881  gxnval  23882  ifbieq12d2  26038  elimifd  26039  elim2if  26040  imadifxp  26073  partfun  26127  resvval2  26431  xrge0iifcnv  26497  xrge0iifcv  26498  xrge0iif1  26502  indval2  26605  ind0  26610  esumpinfval  26656  sigaclfu2  26698  ddeval0  26785  eulerpartlemb  26885  eulerpartlemgs2  26897  ballotlemrv2  27038  plymulx0  27082  signsw0glem  27088  signswmnd  27092  signswlid  27094  signsvtp  27118  signlem0  27122  igamgam  27169  prodeq2ii  27560  prodrblem  27576  fprodcvg  27577  prodmolem2a  27581  zprod  27584  fprodntriv  27589  prodss  27594  fprodsplit  27610  dfrdg2  27743  dfrdg3  27744  unisnif  28090  dfrdg4  28115  mblfinlem2  28567  mbfposadd  28577  itg2addnclem  28581  itg2addnclem2  28582  itg2addnclem3  28583  itg2gt0cn  28585  ibladdnclem  28586  itgaddnclem1  28588  iblabsnclem  28593  iblabsnc  28594  iblmulc2nc  28595  bddiblnc  28600  ftc1anclem5  28609  ftc1anclem6  28610  ftc1anclem7  28611  ftc1anclem8  28612  ftc1anc  28613  areacirclem5  28626  areacirc  28627  fdc  28779  heiborlem4  28851  heiborlem6  28853  ac6s6  29122  pw2f1ocnv  29524  aomclem5  29549  kelac1  29554  flcidc  29669  arearect  29729  areaquad  29730  refsum2cnlem1  29897  afvnfundmuv  30183  clwlkisclwwlklem2fv2  30583  fdmdifeqresdif  30870  suppmptcfin  30931  gsummoncoe1  30985  cply1coe0  30991  cply1coe0bi  30992  dmatmul  31030  scmatsubcl  31038  scmatmulcl  31040  linc1  31066  1elcpmat  31178  m2cpm  31204  m2pminv2lem  31212  pmatcollpw1id  31226  pmatcollpw4fi1lem1  31242  mp2pm2mplem4  31264  chfacffsupp  31310  chfacfscmul0  31312  chfacfpmmul0  31316  ifnmfalse  31394  bj-xpima1sn  32748  riotaclbgBAD  32911  riotaclbBAD  32912  cdleme27a  34317  cdleme31sn2  34339  cdleme31fv2  34343  cdlemefr27cl  34353  dihvalc  35184  mapdhval2  35677  hdmap1val2  35752