Theorem iftruei 4489

Description: Inference associated with iftrue 4488. (Contributed by BJ, 7-Oct-2018.)

Hypothesis

Ref	Expression
iftruei.1	⊢ 𝜑

Assertion

Ref	Expression
iftruei	⊢ if(𝜑, 𝐴, 𝐵) = 𝐴

Proof of Theorem iftruei

Step	Hyp	Ref	Expression
1		iftruei.1	. 2 ⊢ 𝜑
2		iftrue 4488	. 2 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ if(𝜑, 𝐴, 𝐵) = 𝐴

This proof depends on syntax axioms:   = wceq 1570  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4483

This theorem is used by:  oe0m  8519  ttrcltr  9710  ttukeylem4  10583  xnegpnf  13332  xnegmnf  13333  xaddpnf1  13349  xaddpnf2  13350  xaddmnf1  13351  xaddmnf2  13352  pnfaddmnf  13353  mnfaddpnf  13354  xmul01  13390  exp0  14201  swrd00  14785  sgn0  15235  lcm0val  16762  prmo2  17211  prmo3  17212  prmo5  17300  mulg0  19277  zzngim  21851  obsipid  22021  mvrid  22284  mamulid  22749  mamurid  22750  mat1dimid  22782  scmatf1  22839  mdetdiagid  22908  chpdmatlem3  23151  chpidmat  23158  fclscmpi  24341  ioorinv  25890  ig1pval2  26488  dgrcolem2  26586  plydivlem4  26610  vieta1lem2  26627  0cxp  26987  cxpexp  26989  lgs0  27630  lgs2  27634  2lgs2  27725  left1s  28274  exps0  28806  axlowdim  29532  1loopgrvd2  30077  eupth2  30833  ex-prmo  31053  madjusmdetlem1  34452  signsw0glem  35175  breprexp  35255  ex-sategoelel  36165  rdgprc0  36535  bj-pr11val  37898  bj-pr22val  37912  mapdhval0  42762  hdmap1val0  42836  refsum2cnlem1  46023  liminf10ex  46753  cncfiooicclem1  46872  fouriersw  47210  hspmbllem1  47605  blen0  49653  0dig1  49690