Theorem iftrue 2364

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 761	. . 3 |- (ph -> (x e. A <-> ((x e. A /\ ph) \/ (x e. B /\ -. ph))))
2	1	abbi2dv 1577	. 2 |- (ph -> A = {x | ((x e. A /\ ph) \/ (x e. B /\ -. ph))})
3		df-if 2360	. 2 |- if(ph, A, B) = {x | ((x e. A /\ ph) \/ (x e. B /\ -. ph))}
4	2, 3	syl6reqr 1525	1 |- (ph -> if(ph, A, B) = A)

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

This theorem is referenced by:  ifbi 2369  elimif 2372  ifboth 2373  ifid 2374  ifswap 2380  dedth 2381  dedth2v 2382  dedth3v 2383  dedth4v 2384  elimhyp 2388  elimhyp2v 2389  elimhyp3v 2390  elimhyp4v 2391  elimdhyp 2393  keephyp2v 2395  keephyp3v 2396  elimdeloprv 3998  oe0m 4154  suppr 4577  unxpdomlem 4830  xrmax1 5871  xrmax2 5872  xrmin1 5873  xrmin2 5874  max1ALT 5878  icoshftf1olem 6361  exp0t 6521  reret 6760  absmaxt 6862  bcval3tOLD 6925  bcval2t 6926  znnen 7481  ruclem13 7501  ruclem18 7506  ruclem19 7507  metxptval 7811  metxp 7815  dscmet 7901  lmfexlem2 7940  spwval3 8639  cayleythlem 10404

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  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 980  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-if 2360

Copyright terms: Public domain