Theorem iffalse 3902

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 972	. . 3 |- ( -. ph -> ( x e. B <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
2	1	abbi2dv 2581	. 2 |- ( -. ph -> B = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
3		df-if 3894	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
4	2, 3	syl6reqr 2515	1 |- ( -. ph -> if ( ph , A , B ) = B )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 374   /\ wa 375   = wceq 1455   e. wcel 1898   {cab 2448   ifcif 3893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-if 3894

This theorem is referenced by:  iffalsei  3903  iffalsed  3904  ifnefalse  3905  ifsb  3906  ifbi  3914  ifeq1da  3923  ifclda  3925  ifeqda  3926  elimif  3927  ifbothda  3928  ifid  3930  ifnot  3938  ifan  3939  ifor  3940  2if2  3941  ifcomnan  3942  elimhyp  3951  elimhyp2v  3952  elimhyp3v  3953  elimhyp4v  3954  elimdhyp  3956  keephyp2v  3958  keephyp3v  3959  dfopif  4177  opprc  4202  somin1  5252  dfiota4  5593  elimdelov  6399  ovif12  6402  oevn0  7243  pw2f1olem  7702  unxpdomlem2  7803  unxpdomlem3  7804  oi0  8069  wemaplem2  8088  ixpiunwdom  8132  cantnfp1lem3  8211  cantnflem1  8220  dfac12lem2  8600  fin23lem14  8789  axcc2lem  8892  ttukeylem5  8969  uzin  11220  xrmax1  11499  xrmax2  11500  xrmin1  11501  xrmin2  11502  max1ALT  11510  ifle  11519  xmulneg1  11584  modifeq2int  12184  seqf1olem1  12284  seqf1olem2  12285  bcval3  12523  swrdccat  12886  swrdccat3a  12887  swrdccat3b  12889  repswswrd  12924  cshword  12930  ccatco  12969  sumrblem  13826  fsumcvg  13827  summolem2a  13830  sumss  13839  fsumcvg2  13842  sumsplit  13878  prodeq2ii  14016  prodrblem  14032  fprodcvg  14033  prodmolem2a  14037  zprod  14040  prodss  14050  ruclem2  14333  ruclem3  14334  sadadd2lem2  14473  sadcp1  14478  sadcaddlem  14480  gcdn0val  14521  lcmn0val  14608  lcmn0valOLD  14609  lcmfn0val  14642  lcmfn0valOLD  14645  pcgcd  14876  pcmptcl  14885  pcmpt  14886  pcmpt2  14887  pcprod  14889  fldivp1  14891  prmreclem2  14910  prmreclem4  14912  vdwlem6  14985  prmo1  15044  prmop1  15045  fvprmselelfz  15051  fvprmselgcd1  15052  ressval2  15227  xpsaddlem  15530  xpsvsca  15534  setcepi  16032  pmtrmvd  17146  mvrf1  18698  mplcoe3  18739  mplmon2  18765  psrbagsn  18767  evlslem1  18787  obselocv  19340  dmatmul  19571  1mavmul  19622  mulmarep1gsum2  19648  1marepvmarrepid  19649  mdetdiag  19673  mdetrsca2  19678  mdetrlin2  19681  mdetunilem5  19690  mdetunilem7  19692  mdetunilem8  19693  mdetunilem9  19694  mndifsplit  19710  maducoeval2  19714  madugsum  19717  madurid  19718  smadiadetglem2  19746  1elcpmat  19788  decpmatid  19843  ptpjpre1  20635  ptbasfi  20645  isfcls  21073  ptcmplem2  21117  ptcmplem3  21118  dscmet  21636  dscopn  21637  icccmplem2  21890  cnmpt2pc  22005  iccpnfcnv  22021  xrhmeo  22023  pcoval2  22096  pcohtpylem  22099  pcopt  22102  pcopt2  22103  pcoass  22104  pcorevlem  22106  i1f1lem  22696  itg1addlem2  22704  itg1addlem3  22705  i1fres  22712  itg1climres  22721  mbfi1fseqlem4  22725  mbfi1fseqlem5  22726  itg2const2  22748  itg2seq  22749  itg2uba  22750  itg2splitlem  22755  itg2split  22756  itg2monolem1  22757  itg2gt0  22767  itg2cnlem1  22768  itg2cnlem2  22769  iblss  22811  iblss2  22812  itgle  22816  itgss  22818  ibladdlem  22826  itgaddlem1  22829  iblabslem  22834  iblabs  22835  iblabsr  22836  iblmulc2  22837  bddmulibl  22845  ditgneg  22861  elply2  23199  coeeq2  23245  dgrle  23246  coe1termlem  23261  logcnlem3  23638  igamgam  24023  isppw  24090  isnsqf  24111  mule1  24124  sqff1o  24158  chtublem  24188  dchrelbasd  24216  bposlem1  24261  bposlem3  24263  bposlem5  24265  bposlem6  24266  lgsneg  24296  lgsdilem  24299  lgsdir2  24305  lgsdir  24307  lgsdi  24309  lgsne0  24310  dchrvmasum2if  24384  ostth2lem4  24523  axlowdimlem15  25035  ifbieq12d2  28208  elimifd  28209  elim2if  28210  imadifxp  28261  resvval2  28641  xrge0iifcnv  28788  indval2  28885  ddeval0  29107  eulerpartlemb  29250  plymulx0  29485  signsw0glem  29491  signswmnd  29495  dfrdg2  30491  dfrdg3  30492  unisnif  30741  dfrdg4  30767  bj-xpima1sn  31594  finxpreclem2  31827  finxpreclem5  31832  poimirlem15  32000  poimirlem23  32008  mbfposadd  32033  itg2addnclem  32038  itg2addnclem3  32040  itg2gt0cn  32042  ibladdnclem  32043  itgaddnclem1  32045  iblabsnclem  32050  iblabsnc  32051  iblmulc2nc  32052  bddiblnc  32057  ftc1anclem5  32066  ftc1anclem7  32068  ftc1anclem8  32069  ftc1anc  32070  areacirclem5  32081  areacirc  32082  heiborlem4  32191  ac6s6  32460  riotaclbgBAD  32571  cdleme27a  33979  cdleme31sn2  34001  dihvalc  34846  mapdhval2  35339  hdmap1val2  35414  pw2f1ocnv  35937  aomclem5  35961  arearect  36145  areaquad  36146  upbdrech2  37564  lptioo2  37749  lptioo1  37750  coskpi2  37779  cosknegpi  37782  icccncfext  37803  cncfiooicclem1  37809  cncfiooiccre  37811  ioodvbdlimc1lem2  37842  ioodvbdlimc1lem2OLD  37844  ioodvbdlimc2lem  37846  ioodvbdlimc2lemOLD  37847  itgioocnicc  37892  iblcncfioo  37893  dirkerper  37996  dirkertrigeq  38001  dirkercncflem2  38004  fourierdlem10  38017  fourierdlem32  38040  fourierdlem33  38041  fourierdlem37  38045  fourierdlem62  38070  fourierdlem73  38081  fourierdlem74  38082  fourierdlem75  38083  fourierdlem79  38087  fourierdlem81  38089  fourierdlem82  38090  fourierdlem93  38101  fourierdlem97  38105  fourierdlem101  38109  fourierdlem103  38111  fourierdlem104  38112  sqwvfoura  38130  sqwvfourb  38131  fourierswlem  38132  fouriersw  38133  elaa2lem  38135  elaa2lemOLD  38136  etransclem15  38152  etransclem19  38156  etransclem23  38160  etransclem24  38161  etransclem25  38162  nnfoctbdjlem  38331  isomenndlem  38389  volico  38401  ovn0  38426  hsphoidmvle2  38445  hoidmv1lelem1  38451  hoidmv1lelem2  38452  hoidmv1le  38454  hoidmvlelem2  38456  hoidmvlelem3  38457  ovnhoilem1  38461  hspdifhsp  38476  hoidifhspdmvle  38480  hspmbllem1  38486  hspmbllem2  38487  hspmbl  38489  afvnfundmuv  38679  pfxccat3a  39010  cshword2  39018  suppmptcfin  40437  linc1  40491  ifnmfalse  40756