Theorem iffalse 3858

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 963	. . 3 |- ( -. ph -> ( x e. B <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
2	1	abbi2dv 2542	. 2 |- ( -. ph -> B = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
3		df-if 3850	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
4	2, 3	syl6reqr 2476	1 |- ( -. ph -> if ( ph , A , B ) = B )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 369   /\ wa 370   = wceq 1437   e. wcel 1872   {cab 2409   ifcif 3849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-if 3850

This theorem is referenced by:  iffalsei  3859  iffalsed  3860  ifnefalse  3861  ifsb  3862  ifbi  3870  ifeq1da  3879  ifclda  3881  ifeqda  3882  elimif  3883  ifbothda  3884  ifid  3886  ifnot  3894  ifan  3895  ifor  3896  2if2  3897  ifcomnan  3898  elimhyp  3907  elimhyp2v  3908  elimhyp3v  3909  elimhyp4v  3910  elimdhyp  3912  keephyp2v  3914  keephyp3v  3915  dfopif  4122  opprc  4147  somin1  5190  dfiota4  5531  elimdelov  6325  ovif12  6328  oevn0  7167  pw2f1olem  7624  unxpdomlem2  7725  unxpdomlem3  7726  oi0  7991  wemaplem2  8010  ixpiunwdom  8054  cantnfp1lem3  8132  cantnflem1  8141  dfac12lem2  8520  fin23lem14  8709  axcc2lem  8812  ttukeylem5  8889  uzin  11137  xrmax1  11416  xrmax2  11417  xrmin1  11418  xrmin2  11419  max1ALT  11427  ifle  11436  xmulneg1  11501  modifeq2int  12097  seqf1olem1  12197  seqf1olem2  12198  bcval3  12436  swrdccat  12790  swrdccat3a  12791  swrdccat3b  12793  repswswrd  12828  cshword  12834  ccatco  12873  sumrblem  13715  fsumcvg  13716  summolem2a  13719  sumss  13728  fsumcvg2  13731  sumsplit  13767  prodeq2ii  13905  prodrblem  13921  fprodcvg  13922  prodmolem2a  13926  zprod  13929  prodss  13939  ruclem2  14222  ruclem3  14223  sadadd2lem2  14362  sadcp1  14367  sadcaddlem  14369  gcdn0val  14410  lcmn0val  14497  lcmn0valOLD  14498  lcmfn0val  14531  lcmfn0valOLD  14534  pcgcd  14765  pcmptcl  14774  pcmpt  14775  pcmpt2  14776  pcprod  14778  fldivp1  14780  prmreclem2  14799  prmreclem4  14801  vdwlem6  14874  prmo1  14933  prmop1  14934  fvprmselelfz  14940  fvprmselgcd1  14941  ressval2  15116  xpsaddlem  15419  xpsvsca  15423  setcepi  15921  pmtrmvd  17035  mvrf1  18587  mplcoe3  18628  mplmon2  18654  psrbagsn  18656  evlslem1  18676  obselocv  19228  dmatmul  19459  1mavmul  19510  mulmarep1gsum2  19536  1marepvmarrepid  19537  mdetdiag  19561  mdetrsca2  19566  mdetrlin2  19569  mdetunilem5  19578  mdetunilem7  19580  mdetunilem8  19581  mdetunilem9  19582  mndifsplit  19598  maducoeval2  19602  madugsum  19605  madurid  19606  smadiadetglem2  19634  1elcpmat  19676  decpmatid  19731  ptpjpre1  20523  ptbasfi  20533  isfcls  20961  ptcmplem2  21005  ptcmplem3  21006  dscmet  21524  dscopn  21525  icccmplem2  21778  cnmpt2pc  21893  iccpnfcnv  21909  xrhmeo  21911  pcoval2  21984  pcohtpylem  21987  pcopt  21990  pcopt2  21991  pcoass  21992  pcorevlem  21994  i1f1lem  22584  itg1addlem2  22592  itg1addlem3  22593  i1fres  22600  itg1climres  22609  mbfi1fseqlem4  22613  mbfi1fseqlem5  22614  itg2const2  22636  itg2seq  22637  itg2uba  22638  itg2splitlem  22643  itg2split  22644  itg2monolem1  22645  itg2gt0  22655  itg2cnlem1  22656  itg2cnlem2  22657  iblss  22699  iblss2  22700  itgle  22704  itgss  22706  ibladdlem  22714  itgaddlem1  22717  iblabslem  22722  iblabs  22723  iblabsr  22724  iblmulc2  22725  bddmulibl  22733  ditgneg  22749  elply2  23087  coeeq2  23133  dgrle  23134  coe1termlem  23149  logcnlem3  23526  igamgam  23911  isppw  23978  isnsqf  23999  mule1  24012  sqff1o  24046  chtublem  24076  dchrelbasd  24104  bposlem1  24149  bposlem3  24151  bposlem5  24153  bposlem6  24154  lgsneg  24184  lgsdilem  24187  lgsdir2  24193  lgsdir  24195  lgsdi  24197  lgsne0  24198  dchrvmasum2if  24272  ostth2lem4  24411  axlowdimlem15  24923  ifbieq12d2  28100  elimifd  28101  elim2if  28102  imadifxp  28153  resvval2  28539  xrge0iifcnv  28686  indval2  28783  ddeval0  29005  eulerpartlemb  29148  plymulx0  29383  signsw0glem  29389  signswmnd  29393  dfrdg2  30388  dfrdg3  30389  unisnif  30636  dfrdg4  30662  bj-xpima1sn  31460  finxpreclem2  31689  finxpreclem5  31694  poimirlem15  31862  poimirlem23  31870  mbfposadd  31895  itg2addnclem  31900  itg2addnclem3  31902  itg2gt0cn  31904  ibladdnclem  31905  itgaddnclem1  31907  iblabsnclem  31912  iblabsnc  31913  iblmulc2nc  31914  bddiblnc  31919  ftc1anclem5  31928  ftc1anclem7  31930  ftc1anclem8  31931  ftc1anc  31932  areacirclem5  31943  areacirc  31944  heiborlem4  32053  ac6s6  32322  riotaclbgBAD  32438  cdleme27a  33846  cdleme31sn2  33868  dihvalc  34713  mapdhval2  35206  hdmap1val2  35281  pw2f1ocnv  35805  aomclem5  35829  arearect  36013  areaquad  36014  upbdrech2  37423  lptioo2  37594  lptioo1  37595  coskpi2  37624  cosknegpi  37627  icccncfext  37648  cncfiooicclem1  37654  cncfiooiccre  37656  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem2OLD  37689  ioodvbdlimc2lem  37691  ioodvbdlimc2lemOLD  37692  itgioocnicc  37737  iblcncfioo  37738  dirkerper  37841  dirkertrigeq  37846  dirkercncflem2  37849  fourierdlem10  37862  fourierdlem32  37885  fourierdlem33  37886  fourierdlem37  37890  fourierdlem62  37915  fourierdlem73  37926  fourierdlem74  37927  fourierdlem75  37928  fourierdlem79  37932  fourierdlem81  37934  fourierdlem82  37935  fourierdlem93  37946  fourierdlem97  37950  fourierdlem101  37954  fourierdlem103  37956  fourierdlem104  37957  sqwvfoura  37975  sqwvfourb  37976  fourierswlem  37977  fouriersw  37978  elaa2lem  37980  elaa2lemOLD  37981  etransclem15  37997  etransclem19  38001  etransclem23  38005  etransclem24  38006  etransclem25  38007  nnfoctbdjlem  38144  isomenndlem  38202  volico  38210  ovn0  38235  hsphoidmvle2  38254  hoidmv1lelem1  38260  hoidmv1lelem2  38261  hoidmv1le  38263  hoidmvlelem2  38265  hoidmvlelem3  38266  ovnhoilem1  38270  afvnfundmuv  38454  pfxccat3a  38783  cshword2  38791  suppmptcfin  39757  linc1  39811  ifnmfalse  40076