Theorem iffalse 2363

Description: Value of the conditional operator when its first argument is false.

Assertion

Ref	Expression
iffalse	|- (-. ph -> if(ph, A, B) = B)

Proof of Theorem iffalse

Step	Hyp	Ref	Expression
1		dedlemb 762	. . 3 |- (-. ph -> (x e. B <-> ((x e. A /\ ph) \/ (x e. B /\ -. ph))))
2	1	abbi2dv 1575	. 2 |- (-. ph -> B = {x | ((x e. A /\ ph) \/ (x e. B /\ -. ph))})
3		df-if 2358	. 2 |- if(ph, A, B) = {x | ((x e. A /\ ph) \/ (x e. B /\ -. ph))}
4	2, 3	syl6reqr 1523	1 |- (-. ph -> if(ph, A, B) = B)

Syntax hints:  -. wn 2   -> wi 3   \/ wo 222   /\ wa 223   = wceq 954   e. wcel 956  {cab 1461  ifcif 2357

This theorem is referenced by:  ifbi 2367  elimif 2370  ifboth 2371  ifid 2372  ifswap 2378  elimhyp 2386  elimhyp2v 2387  elimhyp3v 2388  elimhyp4v 2389  elimdhyp 2391  keephyp2v 2393  keephyp3v 2394  elimdeloprv 3992  oevn0 4144  suppr 4570  unxpdomlem 4823  xrmax1 5865  xrmax2 5866  xrmin1 5867  xrmin2 5868  max1ALT 5872  expnnvalt 6512  bcval4t 6907  bcclt 6918  znnen 7453  ruclem13 7473  ruclem20 7480  ruclem21 7481  metxpfval 7783  metxp 7786  dscmet 7870  spwnex3 8597

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-if 2358

Copyright terms: Public domain