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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4483

This theorem is used by:  oe0m  8505  ttrcltr  9695  ttukeylem4  10514  xnegpnf  13261  xnegmnf  13262  xaddpnf1  13278  xaddpnf2  13279  xaddmnf1  13280  xaddmnf2  13281  pnfaddmnf  13282  mnfaddpnf  13283  xmul01  13319  exp0  14129  swrd00  14712  sgn0  15162  lcm0val  16684  prmo2  17132  prmo3  17133  prmo5  17221  mulg0  19197  zzngim  21765  obsipid  21935  mvrid  22198  mamulid  22663  mamurid  22664  mat1dimid  22696  scmatf1  22753  mdetdiagid  22822  chpdmatlem3  23065  chpidmat  23072  fclscmpi  24255  ioorinv  25804  ig1pval2  26402  dgrcolem2  26500  plydivlem4  26526  vieta1lem2  26543  0cxp  26903  cxpexp  26905  lgs0  27546  lgs2  27550  2lgs2  27641  left1s  28160  exps0  28692  axlowdim  29418  1loopgrvd2  29963  eupth2  30719  ex-prmo  30939  madjusmdetlem1  34337  signsw0glem  35061  breprexp  35141  ex-sategoelel  36000  rdgprc0  36370  bj-pr11val  37749  bj-pr22val  37763  mapdhval0  42598  hdmap1val0  42672  refsum2cnlem1  45871  liminf10ex  46602  cncfiooicclem1  46721  fouriersw  47059  hspmbllem1  47454  blen0  49502  0dig1  49539