Theorem iffalse 3879

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 953	. . 3 |- ( -. ph -> ( x e. B <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
2	1	abbi2dv 2529	. 2 |- ( -. ph -> B = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
3		df-if 3871	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
4	2, 3	syl6reqr 2452	1 |- ( -. ph -> if ( ph , A , B ) = B )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 366   /\ wa 367   = wceq 1399   e. wcel 1836   {cab 2377   ifcif 3870

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-if 3871

This theorem is referenced by:  iffalsei  3880  iffalsed  3881  ifnefalse  3882  ifsb  3883  ifbi  3891  ifeq1da  3900  ifclda  3902  ifeqda  3903  elimif  3904  ifbothda  3905  ifid  3907  ifnot  3915  ifan  3916  ifor  3917  2if2  3918  ifcomnan  3919  elimhyp  3928  elimhyp2v  3929  elimhyp3v  3930  elimhyp4v  3931  elimdhyp  3933  keephyp2v  3935  keephyp3v  3936  dfopif  4141  opprc  4166  somin1  5326  dfiota4  5501  elimdelov  6295  ovif12  6298  oevn0  7101  pw2f1olem  7558  unxpdomlem2  7659  unxpdomlem3  7660  oi0  7886  wemaplem2  7905  ixpiunwdom  7950  cantnfp1lem3  8030  cantnflem1  8039  cantnfp1lem1OLD  8054  cantnfp1lem3OLD  8056  cantnflem1dOLD  8061  cantnflem1OLD  8062  dfac12lem2  8455  fin23lem14  8644  axcc2lem  8747  ttukeylem5  8824  uzin  11051  xrmax1  11315  xrmax2  11316  xrmin1  11317  xrmin2  11318  max1ALT  11326  ifle  11335  xmulneg1  11400  modifeq2int  11971  seqf1olem1  12068  seqf1olem2  12069  bcval3  12305  swrdccat  12648  swrdccat3a  12649  swrdccat3b  12651  repswswrd  12686  cshword  12692  ccatco  12731  sumrblem  13554  fsumcvg  13555  summolem2a  13558  sumss  13567  fsumcvg2  13570  sumsplit  13604  prodeq2ii  13741  prodrblem  13757  fprodcvg  13758  prodmolem2a  13762  zprod  13765  prodss  13775  ruclem2  13986  ruclem3  13987  sadadd2lem2  14121  sadcp1  14126  sadcaddlem  14128  gcdn0val  14169  pcgcd  14422  pcmptcl  14431  pcmpt  14432  pcmpt2  14433  pcprod  14435  fldivp1  14437  prmreclem2  14456  prmreclem4  14458  vdwlem6  14525  ressval2  14709  xpsaddlem  15001  xpsvsca  15005  setcepi  15503  pmtrmvd  16617  gsumval3aOLD  17042  gsumzsplitOLD  17081  dmdprdsplitlemOLD  17217  psrlidmOLD  18189  psrridmOLD  18191  mvridlemOLD  18207  mvrf1  18213  mplcoe3  18260  mplcoe3OLD  18261  mplcoe2OLD  18265  mplmon2  18290  psrbagsn  18292  evlslem1  18316  obselocv  18869  dmatmul  19103  1mavmul  19154  mulmarep1gsum2  19180  1marepvmarrepid  19181  mdetdiag  19205  mdetrsca2  19210  mdetrlin2  19213  mdetunilem5  19222  mdetunilem7  19224  mdetunilem8  19225  mdetunilem9  19226  mndifsplit  19242  maducoeval2  19246  madugsum  19249  madurid  19250  smadiadetglem2  19278  1elcpmat  19320  decpmatid  19375  ptpjpre1  20176  ptbasfi  20186  isfcls  20614  ptcmplem2  20657  ptcmplem3  20658  dscmet  21197  dscopn  21198  icccmplem2  21432  cnmpt2pc  21532  iccpnfcnv  21548  xrhmeo  21550  pcoval2  21620  pcohtpylem  21623  pcopt  21626  pcopt2  21627  pcoass  21628  pcorevlem  21630  i1f1lem  22200  itg1addlem2  22208  itg1addlem3  22209  i1fres  22216  itg1climres  22225  mbfi1fseqlem4  22229  mbfi1fseqlem5  22230  itg2const2  22252  itg2seq  22253  itg2uba  22254  itg2splitlem  22259  itg2split  22260  itg2monolem1  22261  itg2gt0  22271  itg2cnlem1  22272  itg2cnlem2  22273  iblss  22315  iblss2  22316  itgle  22320  itgss  22322  ibladdlem  22330  itgaddlem1  22333  iblabslem  22338  iblabs  22339  iblabsr  22340  iblmulc2  22341  bddmulibl  22349  ditgneg  22365  elply2  22697  coeeq2  22743  dgrle  22744  coe1termlem  22759  logcnlem3  23131  isppw  23524  isnsqf  23545  mule1  23558  sqff1o  23592  chtublem  23622  dchrelbasd  23650  bposlem1  23695  bposlem3  23697  bposlem5  23699  bposlem6  23700  lgsneg  23730  lgsdilem  23733  lgsdir2  23739  lgsdir  23741  lgsdi  23743  lgsne0  23744  dchrvmasum2if  23818  ostth2lem4  23957  axlowdimlem15  24401  ifbieq12d2  27568  elimifd  27569  elim2if  27570  imadifxp  27621  resvval2  28004  xrge0iifcnv  28100  indval2  28194  ddeval0  28399  eulerpartlemb  28526  plymulx0  28723  signsw0glem  28729  signswmnd  28733  igamgam  28816  dfrdg2  29429  dfrdg3  29430  unisnif  29764  dfrdg4  29789  mbfposadd  30263  itg2addnclem  30268  itg2addnclem3  30270  itg2gt0cn  30272  ibladdnclem  30273  itgaddnclem1  30275  iblabsnclem  30280  iblabsnc  30281  iblmulc2nc  30282  bddiblnc  30287  ftc1anclem5  30296  ftc1anclem7  30298  ftc1anclem8  30299  ftc1anc  30300  areacirclem5  30313  areacirc  30314  heiborlem4  30512  ac6s6  30782  pw2f1ocnv  31181  aomclem5  31206  arearect  31387  areaquad  31388  lcmn0val  31405  upbdrech2  31709  lptioo2  31838  lptioo1  31839  coskpi2  31867  cosknegpi  31870  icccncfext  31891  cncfiooicclem1  31897  cncfiooiccre  31899  ioodvbdlimc1lem2  31930  ioodvbdlimc2lem  31932  itgioocnicc  31977  iblcncfioo  31978  dirkerper  32079  dirkertrigeq  32084  dirkercncflem2  32087  fourierdlem10  32100  fourierdlem32  32122  fourierdlem33  32123  fourierdlem37  32127  fourierdlem62  32152  fourierdlem73  32163  fourierdlem74  32164  fourierdlem75  32165  fourierdlem79  32169  fourierdlem81  32171  fourierdlem82  32172  fourierdlem93  32183  fourierdlem97  32187  fourierdlem101  32191  fourierdlem103  32193  fourierdlem104  32194  sqwvfoura  32212  sqwvfourb  32213  fourierswlem  32214  fouriersw  32215  elaa2lem  32217  etransclem15  32233  etransclem19  32237  etransclem23  32241  etransclem24  32242  etransclem25  32243  afvnfundmuv  32425  pfxccat3a  32639  cshword2  32647  suppmptcfin  33207  linc1  33261  ifnmfalse  33528  bj-xpima1sn  34896  riotaclbgBAD  35133  cdleme27a  36541  cdleme31sn2  36563  dihvalc  37408  mapdhval2  37901  hdmap1val2  37976