Theorem iffalse 3941

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 948	. . 3 |- ( -. ph -> ( x e. B <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
2	1	abbi2dv 2597	. 2 |- ( -. ph -> B = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
3		df-if 3933	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
4	2, 3	syl6reqr 2520	1 |- ( -. ph -> if ( ph , A , B ) = B )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 368   /\ wa 369   = wceq 1374   e. wcel 1762   {cab 2445   ifcif 3932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-if 3933

This theorem is referenced by:  iffalsei  3942  iffalsed  3943  ifnefalse  3944  ifsb  3945  ifbi  3953  ifeq1da  3962  ifclda  3964  ifeqda  3965  elimif  3966  ifbothda  3967  ifid  3969  ifeqor  3976  ifnot  3977  ifan  3978  ifor  3979  2if2  3980  ifcomnan  3981  elimhyp  3991  elimhyp2v  3992  elimhyp3v  3993  elimhyp4v  3994  elimdhyp  3996  keephyp2v  3998  keephyp3v  3999  dfopif  4203  opprc  4228  somin1  5394  somincom  5395  dfiota4  5570  elimdelov  6353  ovif12  6356  mpt2difsnif  6370  tz7.44-2  7063  tz7.44-3  7064  oevn0  7155  pw2f1olem  7611  unxpdomlem2  7715  unxpdomlem3  7716  sniffsupp  7858  oi0  7942  wemaplem2  7961  unwdomg  7999  ixpiunwdom  8006  cantnfp1lem1  8086  cantnfp1lem3  8088  cantnflem1d  8096  cantnflem1  8097  cantnfp1lem1OLD  8112  cantnfp1lem3OLD  8114  cantnflem1dOLD  8119  cantnflem1OLD  8120  dfac12lem2  8513  fin23lem14  8702  axcc2lem  8805  ttukeylem5  8882  ttukeylem7  8884  canthp1lem2  9020  pwfseqlem3  9027  uzin  11103  xrmax1  11365  xrmax2  11366  xrmin1  11367  xrmin2  11368  max1ALT  11376  ifle  11385  xmulneg1  11450  rexmul  11452  xmulpnf1  11455  fzprval  11729  modifeq2int  12005  seqf1olem1  12102  seqf1olem2  12103  expnnval  12125  expneg  12130  bcval3  12339  ccatval2  12548  lswccatn0lsw  12558  swrdnd  12607  swrd0  12608  swrdvalodm2  12614  swrdvalodm  12615  swrdccatin2  12662  swrdccat  12668  swrdccat3a  12669  swrdccat3b  12671  repswswrd  12706  cshword  12712  ccatco  12751  sgnp  12873  sgnn  12877  absmax  13111  sumeq2ii  13464  sumrblem  13482  fsumcvg  13483  summolem2a  13486  sumss  13495  sumss2  13497  fsumcvg2  13498  fsumsplit  13511  sumsplit  13532  ef0lem  13665  rpnnen2lem9  13806  ruclem2  13815  ruclem3  13816  sadadd2lem2  13948  sadcp1  13953  sadcaddlem  13955  sadadd2  13958  gcdn0val  13996  eucalgf  14060  eucalginv  14061  eucalglt  14062  iserodd  14207  pcgcd  14249  pcmptcl  14258  pcmpt  14259  pcmpt2  14260  pcprod  14262  fldivp1  14264  prmreclem2  14283  prmreclem4  14285  vdwlem6  14352  ramtub  14378  ressval2  14533  xpsaddlem  14819  xpsvsca  14823  setcepi  15262  gsumval2a  15818  mulgnn  15941  mulgnegnn  15945  symgextfv  16231  pmtrprfv3  16268  pmtrmvd  16270  pmtrdifellem4  16293  pmtrprfval  16301  pmtrprfvalrn  16302  odlem2  16352  dfod2  16375  gsumval3a  16689  gsumval3aOLD  16690  gsumzsplit  16728  gsumzsplitOLD  16729  dmdprdsplitlem  16867  dmdprdsplitlemOLD  16868  abvtrivd  17265  psrlidm  17820  psrlidmOLD  17821  psrridm  17822  psrridmOLD  17823  mvridlemOLD  17839  mvrf1  17845  mvrcl  17875  mplmon  17889  mplmonmul  17890  mplcoe1  17891  mplcoe3  17892  mplcoe3OLD  17893  mplcoe5  17895  mplcoe2OLD  17897  mplmon2  17922  psrbagsn  17924  evlslem3  17947  evlslem1  17948  coe1tmfv2  18080  cply1coe0  18105  cply1coe0bi  18106  obselocv  18519  uvcvv0  18581  uvcff  18582  dmatmul  18759  1mavmul  18810  mulmarep1gsum1  18835  mulmarep1gsum2  18836  1marepvmarrepid  18837  1marepvsma1  18845  mdetdiag  18861  mdetrsca2  18866  mdetrlin2  18869  mdetunilem2  18875  mdetunilem5  18878  mdetunilem7  18880  mdetunilem8  18881  mdetunilem9  18882  mndifsplit  18898  maducoeval2  18902  madugsum  18905  madurid  18906  symgmatr01lem  18915  gsummatr01lem3  18919  gsummatr01lem4  18920  gsummatr01  18921  smadiadetglem2  18934  1elcpmat  18976  m2cpm  19002  m2cpminvid2lem  19015  decpmatid  19031  pmatcollpw3fi1lem1  19047  chfacfscmul0  19119  chfacfpmmul0  19123  ptpjpre1  19800  ptpjpre2  19809  ptbasfi  19810  ptopn2  19813  xkopt  19884  isfcls  20238  ptcmplem2  20281  ptcmplem3  20282  tsmssplit  20382  dscmet  20821  dscopn  20822  xrsxmet  21042  icccmplem2  21056  cnmpt2pc  21156  iccpnfcnv  21172  xrhmeo  21174  htpycc  21208  pco1  21243  pcoval2  21244  pcohtpylem  21247  pcopt  21250  pcopt2  21251  pcoass  21252  pcorevlem  21254  ovolunlem1a  21635  ovolunlem1  21636  ovolicc1  21655  i1f1lem  21824  itg11  21826  itg1addlem2  21832  itg1addlem3  21833  i1fres  21840  itg1climres  21849  mbfi1fseqlem4  21853  mbfi1fseqlem5  21854  mbfi1flim  21858  itg2const2  21876  itg2seq  21877  itg2uba  21878  itg2splitlem  21883  itg2split  21884  itg2monolem1  21885  itg2gt0  21895  itg2cnlem1  21896  itg2cnlem2  21897  itgeq2  21912  iblss  21939  iblss2  21940  itgle  21944  itgss  21946  itgss2  21947  itgss3  21949  itgless  21951  ibladdlem  21954  itgaddlem1  21957  iblabslem  21962  iblabs  21963  iblabsr  21964  iblmulc2  21965  bddmulibl  21973  itggt0  21976  itgcn  21977  ditgneg  21989  limccnp2  22024  dvexp2  22085  lhop2  22144  deg1add  22232  ig1pval3  22303  elply2  22321  ply1termlem  22328  plyeq0lem  22335  plypf1  22337  coeeq2  22367  dgrle  22368  coe1termlem  22382  dvply1  22407  pserdvlem2  22550  abelthlem9  22562  logcnlem3  22746  logtayllem  22761  logtayl  22762  cxpef  22767  rlimcnp2  23017  efrlim  23020  isppw  23109  isnsqf  23130  mule1  23143  sqff1o  23177  muinv  23190  chtublem  23207  dchrelbasd  23235  bposlem1  23280  bposlem3  23282  bposlem5  23284  bposlem6  23285  lgsval2lem  23302  lgsval4  23312  lgsval4a  23314  lgsneg  23315  lgsneg1  23316  lgsdilem  23318  lgsdir2  23324  lgsdir  23326  lgsdi  23328  lgsne0  23329  rplogsumlem2  23391  dchrvmasum2if  23403  dchrisum0fno1  23417  rplogsum  23433  pntrlog2bndlem4  23486  pntrlog2bndlem5  23487  padicabv  23536  ostth1  23539  ostth2lem4  23542  ostth3  23544  axlowdimlem15  23928  axlowdim  23933  clwlkisclwwlklem2fv2  24445  gxpval  24787  gxnval  24788  ifbieq12d2  26944  elimifd  26945  elim2if  26946  imadifxp  26981  partfun  27038  resvval2  27332  xrge0iifcnv  27401  xrge0iifcv  27402  xrge0iif1  27406  indval2  27518  ind0  27523  esumpinfval  27569  sigaclfu2  27611  ddeval0  27697  eulerpartlemb  27797  eulerpartlemgs2  27809  ballotlemrv2  27950  plymulx0  27994  signsw0glem  28000  signswmnd  28004  signswlid  28006  signsvtp  28030  signlem0  28034  igamgam  28081  prodeq2ii  28472  prodrblem  28488  fprodcvg  28489  prodmolem2a  28493  zprod  28496  fprodntriv  28501  prodss  28506  fprodsplit  28522  dfrdg2  28655  dfrdg3  28656  unisnif  29002  dfrdg4  29027  mblfinlem2  29480  mbfposadd  29490  itg2addnclem  29494  itg2addnclem2  29495  itg2addnclem3  29496  itg2gt0cn  29498  ibladdnclem  29499  itgaddnclem1  29501  iblabsnclem  29506  iblabsnc  29507  iblmulc2nc  29508  bddiblnc  29513  ftc1anclem5  29522  ftc1anclem6  29523  ftc1anclem7  29524  ftc1anclem8  29525  ftc1anc  29526  areacirclem5  29539  areacirc  29540  fdc  29692  heiborlem4  29764  heiborlem6  29766  ac6s6  30035  pw2f1ocnv  30436  aomclem5  30461  kelac1  30466  flcidc  30581  arearect  30641  areaquad  30642  refsum2cnlem1  30809  ifeq123d  30833  upbdrech2  30904  ioondisj2  30908  lptioo2  30992  lptioo1  30993  coskpi2  31021  cosknegpi  31024  icccncfext  31045  cncfiooicclem1  31051  cncfiooiccre  31053  ioodvbdlimc1lem2  31081  ioodvbdlimc2lem  31083  ditgeqiooicc  31097  iblempty  31102  itgioocnicc  31114  iblcncfioo  31115  dirkerper  31215  dirkertrigeq  31220  dirkercncflem2  31223  dirkercncflem4  31225  fourierdlem9  31235  fourierdlem10  31236  fourierdlem17  31243  fourierdlem32  31258  fourierdlem33  31259  fourierdlem37  31263  fourierdlem40  31266  fourierdlem43  31269  fourierdlem62  31288  fourierdlem65  31291  fourierdlem73  31299  fourierdlem74  31300  fourierdlem75  31301  fourierdlem76  31302  fourierdlem78  31304  fourierdlem79  31305  fourierdlem81  31307  fourierdlem82  31308  fourierdlem91  31317  fourierdlem93  31319  fourierdlem97  31323  fourierdlem101  31327  fourierdlem103  31329  fourierdlem104  31330  sqwvfoura  31348  sqwvfourb  31349  fourierswlem  31350  fouriersw  31351  afvnfundmuv  31510  fdmdifeqresdif  31870  suppmptcfin  31920  linc1  31974  ifnmfalse  32113  bj-xpima1sn  33469  riotaclbgBAD  33632  riotaclbBAD  33633  cdleme27a  35038  cdleme31sn2  35060  cdleme31fv2  35064  cdlemefr27cl  35074  dihvalc  35905  mapdhval2  36398  hdmap1val2  36473