Theorem iftrue 2370

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 764	. . 3 |- (ph -> (x e. A <-> ((x e. A /\ ph) \/ (x e. B /\ -. ph))))
2	1	abbi2dv 1581	. 2 |- (ph -> A = {x | ((x e. A /\ ph) \/ (x e. B /\ -. ph))})
3		df-if 2366	. 2 |- if(ph, A, B) = {x | ((x e. A /\ ph) \/ (x e. B /\ -. ph))}
4	2, 3	syl6reqr 1529	1 |- (ph -> if(ph, A, B) = A)

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

This theorem is referenced by:  ifbi 2375  elimif 2378  ifboth 2379  ifid 2380  ifswap 2386  dedth 2387  dedth2v 2388  dedth3v 2389  dedth4v 2390  elimhyp 2394  elimhyp2v 2395  elimhyp3v 2396  elimhyp4v 2397  elimdhyp 2399  keephyp2v 2401  keephyp3v 2402  elimdeloprv 4007  oe0m 4163  suppr 4599  unxpdomlem 4854  xrmax1 5911  xrmax2 5912  xrmin1 5913  xrmin2 5914  max1ALT 5918  icoshftf1olem 6411  exp0t 6572  absmaxt 6897  bcval2t 6959  znnen 7503  ruclem13 7523  ruclem18 7528  ruclem19 7529  metxptval 7827  metxp 7831  dscmet 7915  lmfexlem2 7954  spwval3 8650  cayleythlem 10408

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-if 2366

Copyright terms: Public domain