Theorem iftrue 2366

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

Assertion

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

Proof of Theorem iftrue

Step	Hyp	Ref	Expression
1		dedlema 762	. . 3 |- (ph -> (x e. A <-> ((x e. A /\ ph) \/ (x e. B /\ -. ph))))
2	1	abbi2dv 1578	. 2 |- (ph -> A = {x | ((x e. A /\ ph) \/ (x e. B /\ -. ph))})
3		df-if 2362	. 2 |- if(ph, A, B) = {x | ((x e. A /\ ph) \/ (x e. B /\ -. ph))}
4	2, 3	syl6reqr 1526	1 |- (ph -> if(ph, A, B) = A)

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

This theorem is referenced by:  ifbi 2371  elimif 2374  ifboth 2375  ifid 2376  ifswap 2382  dedth 2383  dedth2v 2384  dedth3v 2385  dedth4v 2386  elimhyp 2390  elimhyp2v 2391  elimhyp3v 2392  elimhyp4v 2393  elimdhyp 2395  keephyp2v 2397  keephyp3v 2398  elimdeloprv 4001  oe0m 4157  suppr 4590  unxpdomlem 4843  xrmax1 5909  xrmax2 5910  xrmin1 5911  xrmin2 5912  max1ALT 5916  icoshftf1olem 6410  exp0t 6571  absmaxt 6897  bcval2t 6959  znnen 7502  ruclem13 7522  ruclem18 7527  ruclem19 7528  metxptval 7830  metxp 7834  dscmet 7918  lmfexlem2 7957  spwval3 8654  cayleythlem 10413

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-if 2362

Copyright terms: Public domain