Theorem iffalse 3931

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

Syntax hints:   -. wn 3   -> wi 4   \/ wo 368   /\ wa 369   = wceq 1381   e. wcel 1802   {cab 2426   ifcif 3922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-if 3923

This theorem is referenced by:  iffalsei  3932  iffalsed  3933  ifnefalse  3934  ifsb  3935  ifbi  3943  ifeq1da  3952  ifclda  3954  ifeqda  3955  elimif  3956  ifbothda  3957  ifid  3959  ifnot  3967  ifan  3968  ifor  3969  2if2  3970  ifcomnan  3971  elimhyp  3981  elimhyp2v  3982  elimhyp3v  3983  elimhyp4v  3984  elimdhyp  3986  keephyp2v  3988  keephyp3v  3989  dfopif  4195  opprc  4220  somin1  5389  dfiota4  5565  elimdelov  6359  ovif12  6362  oevn0  7163  pw2f1olem  7619  unxpdomlem2  7723  unxpdomlem3  7724  oi0  7951  wemaplem2  7970  ixpiunwdom  8015  cantnfp1lem3  8097  cantnflem1  8106  cantnfp1lem1OLD  8121  cantnfp1lem3OLD  8123  cantnflem1dOLD  8128  cantnflem1OLD  8129  dfac12lem2  8522  fin23lem14  8711  axcc2lem  8814  ttukeylem5  8891  uzin  11117  xrmax1  11380  xrmax2  11381  xrmin1  11382  xrmin2  11383  max1ALT  11391  ifle  11400  xmulneg1  11465  modifeq2int  12023  seqf1olem1  12120  seqf1olem2  12121  bcval3  12358  swrdccat  12692  swrdccat3a  12693  swrdccat3b  12695  repswswrd  12730  cshword  12736  ccatco  12775  sumrblem  13507  fsumcvg  13508  summolem2a  13511  sumss  13520  fsumcvg2  13523  sumsplit  13557  ruclem2  13837  ruclem3  13838  sadadd2lem2  13972  sadcp1  13977  sadcaddlem  13979  gcdn0val  14020  pcgcd  14273  pcmptcl  14282  pcmpt  14283  pcmpt2  14284  pcprod  14286  fldivp1  14288  prmreclem2  14307  prmreclem4  14309  vdwlem6  14376  ressval2  14558  xpsaddlem  14844  xpsvsca  14848  setcepi  15284  pmtrmvd  16350  gsumval3aOLD  16775  gsumzsplitOLD  16814  dmdprdsplitlemOLD  16953  psrlidmOLD  17925  psrridmOLD  17927  mvridlemOLD  17943  mvrf1  17949  mplcoe3  17996  mplcoe3OLD  17997  mplcoe2OLD  18001  mplmon2  18026  psrbagsn  18028  evlslem1  18052  obselocv  18626  dmatmul  18866  1mavmul  18917  mulmarep1gsum2  18943  1marepvmarrepid  18944  mdetdiag  18968  mdetrsca2  18973  mdetrlin2  18976  mdetunilem5  18985  mdetunilem7  18987  mdetunilem8  18988  mdetunilem9  18989  mndifsplit  19005  maducoeval2  19009  madugsum  19012  madurid  19013  smadiadetglem2  19041  1elcpmat  19083  decpmatid  19138  ptpjpre1  19938  ptbasfi  19948  isfcls  20376  ptcmplem2  20419  ptcmplem3  20420  dscmet  20959  dscopn  20960  icccmplem2  21194  cnmpt2pc  21294  iccpnfcnv  21310  xrhmeo  21312  pcoval2  21382  pcohtpylem  21385  pcopt  21388  pcopt2  21389  pcoass  21390  pcorevlem  21392  i1f1lem  21962  itg1addlem2  21970  itg1addlem3  21971  i1fres  21978  itg1climres  21987  mbfi1fseqlem4  21991  mbfi1fseqlem5  21992  itg2const2  22014  itg2seq  22015  itg2uba  22016  itg2splitlem  22021  itg2split  22022  itg2monolem1  22023  itg2gt0  22033  itg2cnlem1  22034  itg2cnlem2  22035  iblss  22077  iblss2  22078  itgle  22082  itgss  22084  ibladdlem  22092  itgaddlem1  22095  iblabslem  22100  iblabs  22101  iblabsr  22102  iblmulc2  22103  bddmulibl  22111  ditgneg  22127  elply2  22459  coeeq2  22505  dgrle  22506  coe1termlem  22520  logcnlem3  22890  isppw  23253  isnsqf  23274  mule1  23287  sqff1o  23321  chtublem  23351  dchrelbasd  23379  bposlem1  23424  bposlem3  23426  bposlem5  23428  bposlem6  23429  lgsneg  23459  lgsdilem  23462  lgsdir2  23468  lgsdir  23470  lgsdi  23472  lgsne0  23473  dchrvmasum2if  23547  ostth2lem4  23686  axlowdimlem15  24124  ifbieq12d2  27285  elimifd  27286  elim2if  27287  imadifxp  27323  resvval2  27685  xrge0iifcnv  27781  indval2  27894  ddeval0  28073  eulerpartlemb  28173  plymulx0  28370  signsw0glem  28376  signswmnd  28380  igamgam  28457  prodeq2ii  29013  prodrblem  29029  fprodcvg  29030  prodmolem2a  29034  zprod  29037  prodss  29047  dfrdg2  29196  dfrdg3  29197  unisnif  29543  dfrdg4  29568  mbfposadd  30030  itg2addnclem  30034  itg2addnclem3  30036  itg2gt0cn  30038  ibladdnclem  30039  itgaddnclem1  30041  iblabsnclem  30046  iblabsnc  30047  iblmulc2nc  30048  bddiblnc  30053  ftc1anclem5  30062  ftc1anclem7  30064  ftc1anclem8  30065  ftc1anc  30066  areacirclem5  30079  areacirc  30080  heiborlem4  30278  ac6s6  30548  pw2f1ocnv  30947  aomclem5  30972  arearect  31152  areaquad  31153  lcmn0val  31170  upbdrech2  31453  lptioo2  31541  lptioo1  31542  coskpi2  31569  cosknegpi  31572  icccncfext  31593  cncfiooicclem1  31599  cncfiooiccre  31601  ioodvbdlimc1lem2  31629  ioodvbdlimc2lem  31631  itgioocnicc  31662  iblcncfioo  31663  dirkerper  31763  dirkertrigeq  31768  dirkercncflem2  31771  fourierdlem10  31784  fourierdlem32  31806  fourierdlem33  31807  fourierdlem37  31811  fourierdlem62  31836  fourierdlem73  31847  fourierdlem74  31848  fourierdlem75  31849  fourierdlem79  31853  fourierdlem81  31855  fourierdlem82  31856  fourierdlem93  31867  fourierdlem97  31871  fourierdlem101  31875  fourierdlem103  31877  fourierdlem104  31878  sqwvfoura  31896  sqwvfourb  31897  fourierswlem  31898  fouriersw  31899  afvnfundmuv  32058  suppmptcfin  32682  linc1  32736  ifnmfalse  32867  bj-xpima1sn  34225  riotaclbgBAD  34387  cdleme27a  35795  cdleme31sn2  35817  dihvalc  36662  mapdhval2  37155  hdmap1val2  37230