Theorem iffalse 3706

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 922	. . 3 |- ( -. ph -> ( x e. B <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
2	1	abbi2dv 2519	. 2 |- ( -. ph -> B = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
3		df-if 3700	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
4	2, 3	syl6reqr 2455	1 |- ( -. ph -> if ( ph , A , B ) = B )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 358   /\ wa 359   = wceq 1649   e. wcel 1721   {cab 2390   ifcif 3699

This theorem is referenced by:  ifnefalse  3707  ifsb  3708  ifbi  3716  ifeq1da  3724  ifclda  3726  elimif  3728  ifbothda  3729  ifid  3731  ifeqor  3736  ifnot  3737  ifan  3738  ifor  3739  elimhyp  3747  elimhyp2v  3748  elimhyp3v  3749  elimhyp4v  3750  elimdhyp  3752  keephyp2v  3754  keephyp3v  3755  dfopif  3941  opprc  3965  somin1  5229  somincom  5230  dfiota4  5405  elimdelov  6112  riotav  6513  riotaund  6545  tz7.44-2  6624  tz7.44-3  6625  oevn0  6718  pw2f1olem  7171  unxpdomlem2  7273  unxpdomlem3  7274  oi0  7453  wemaplem2  7472  unwdomg  7508  ixpiunwdom  7515  cantnfp1lem1  7590  cantnfp1lem3  7592  cantnflem1d  7600  cantnflem1  7601  dfac12lem2  7980  fin23lem14  8169  axcc2lem  8272  ttukeylem5  8349  ttukeylem7  8351  canthp1lem2  8484  pwfseqlem3  8491  uzin  10474  xrmax1  10719  xrmax2  10720  xrmin1  10721  xrmin2  10722  max1ALT  10730  ifle  10739  xmulneg1  10804  rexmul  10806  xmulpnf1  10809  fzprval  11062  seqf1olem1  11317  seqf1olem2  11318  expnnval  11340  expneg  11344  bcval3  11552  ccatval2  11701  ccatco  11759  absmax  12088  sumeq2ii  12442  sumrblem  12460  fsumcvg  12461  summolem2a  12464  zsum  12467  sum0  12470  sumss  12473  sumss2  12475  fsumcvg2  12476  fsumsplit  12488  sumsplit  12507  ef0lem  12636  rpnnen2lem9  12777  ruclem2  12786  ruclem3  12787  sadadd2lem2  12917  sadcp1  12922  sadcaddlem  12924  sadadd2  12927  gcdn0val  12965  eucalgf  13029  eucalginv  13030  eucalglt  13031  iserodd  13164  pcgcd  13206  pcmptcl  13215  pcmpt  13216  pcmpt2  13217  pcprod  13219  fldivp1  13221  prmreclem2  13240  prmreclem4  13242  vdwlem6  13309  ramtub  13335  ressval2  13473  xpsaddlem  13755  xpsvsca  13759  setcepi  14198  gsumval2a  14737  mulgnn  14851  mulgnegnn  14855  odlem2  15132  dfod2  15155  gsumval3a  15467  gsumzsplit  15484  dmdprdsplitlem  15550  abvtrivd  15883  psrlidm  16422  psrridm  16423  mvridlem  16438  mvrf1  16444  mvrcl  16467  mplmon  16481  mplmonmul  16482  mplcoe1  16483  mplcoe3  16484  mplcoe2  16485  mplmon2  16508  psrbagsn  16510  coe1tmfv2  16622  obselocv  16910  ptpjpre1  17556  ptpjpre2  17565  ptbasfi  17566  ptopn2  17569  xkopt  17640  isfcls  17994  ptcmplem2  18037  ptcmplem3  18038  tsmssplit  18134  dscmet  18573  dscopn  18574  xrsxmet  18793  icccmplem2  18807  cnmpt2pc  18906  iccpnfcnv  18922  xrhmeo  18924  htpycc  18958  pco1  18993  pcoval2  18994  pcohtpylem  18997  pcopt  19000  pcopt2  19001  pcoass  19002  pcorevlem  19004  ovolunlem1a  19345  ovolunlem1  19346  ovolicc1  19365  i1f1lem  19534  itg11  19536  itg1addlem2  19542  itg1addlem3  19543  i1fres  19550  itg1climres  19559  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  mbfi1flim  19568  itg2const2  19586  itg2seq  19587  itg2uba  19588  itg2splitlem  19593  itg2split  19594  itg2monolem1  19595  itg2gt0  19605  itg2cnlem1  19606  itg2cnlem2  19607  itgeq2  19622  itg0  19624  iblss  19649  iblss2  19650  itgle  19654  itgss  19656  itgss2  19657  itgss3  19659  itgless  19661  ibladdlem  19664  itgaddlem1  19667  iblabslem  19672  iblabs  19673  iblabsr  19674  iblmulc2  19675  bddmulibl  19683  itggt0  19686  itgcn  19687  ditgneg  19697  limccnp2  19732  dvexp2  19793  lhop2  19852  evlslem3  19888  evlslem1  19889  deg1add  19979  ig1pval3  20050  elply2  20068  ply1termlem  20075  plyeq0lem  20082  plypf1  20084  coeeq2  20114  dgrle  20115  coe1termlem  20129  dvply1  20154  vieta1lem2  20181  pserdvlem2  20297  abelthlem9  20309  logcnlem3  20488  logtayllem  20503  logtayl  20504  cxpef  20509  rlimcnp2  20758  efrlim  20761  isppw  20850  isnsqf  20871  mule1  20884  sqff1o  20918  muinv  20931  chtublem  20948  dchrelbasd  20976  bposlem1  21021  bposlem3  21023  bposlem5  21025  bposlem6  21026  lgsval2lem  21043  lgsval4  21053  lgsval4a  21055  lgsneg  21056  lgsneg1  21057  lgsdilem  21059  lgsdir2  21065  lgsdir  21067  lgsdi  21069  lgsne0  21070  rplogsumlem2  21132  dchrvmasum2if  21144  dchrisum0fno1  21158  rplogsum  21174  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  padicabv  21277  ostth1  21280  ostth2lem4  21283  ostth3  21285  gxpval  21800  gxnval  21801  ifbieq12d2  23955  elimifd  23957  elim2if  23958  imadifxp  23991  partfun  24040  xrge0iifcnv  24272  xrge0iifcv  24273  xrge0iif1  24277  indval2  24365  ind0  24370  esumpinfval  24416  sigaclfu2  24457  ballotlemrv2  24732  igamgam  24786  prodeq2ii  25192  prodrblem  25208  fprodcvg  25209  prodmolem2a  25213  zprod  25216  fprodntriv  25221  prod0  25222  prodss  25226  fprodsplit  25242  dfrdg2  25366  dfrdg3  25367  unisnif  25678  dfrdg4  25703  axlowdimlem15  25799  axlowdim  25804  mblfinlem  26143  mbfposadd  26153  itg2addnclem  26155  itg2addnclem2  26156  itg2addnclem3  26157  itg2gt0cn  26159  ibladdnclem  26160  itgaddnclem1  26162  iblabsnclem  26167  iblabsnc  26168  iblmulc2nc  26169  bddiblnc  26174  areacirclem6  26186  areacirc  26187  fdc  26339  heiborlem4  26413  heiborlem6  26415  pw2f1ocnv  26998  aomclem5  27023  kelac1  27029  uvcvv0  27107  uvcff  27108  flcidc  27247  pmtrmvd  27266  mamulid  27326  mamurid  27327  refsum2cnlem1  27575  afvnfundmuv  27870  2if2  27941  swrdnd  28001  swrd0  28002  swrdccat3a  28030  swrdccat3b  28031  ifnmfalse  28220  sgnp  28234  sgnn  28238  cdleme27a  30849  cdleme31sn2  30871  cdleme31fv2  30875  cdlemefr27cl  30885  dihvalc  31716  mapdhval2  32209  hdmap1val2  32284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-if 3700