Theorem iftruei 4488

Description: Inference associated with iftrue 4487. (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 4487	. 2 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ if(𝜑, 𝐴, 𝐵) = 𝐴

This proof depends on syntax axioms:   = wceq 1569  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  oe0m  8531  ttrcltr  9722  ttukeylem4  10595  xnegpnf  13344  xnegmnf  13345  xaddpnf1  13361  xaddpnf2  13362  xaddmnf1  13363  xaddmnf2  13364  pnfaddmnf  13365  mnfaddpnf  13366  xmul01  13402  exp0  14213  swrd00  14798  sgn0  15249  lcm0val  16776  prmo2  17225  prmo3  17226  prmo5  17314  mulg0  19291  zzngim  21865  obsipid  22035  mvrid  22298  mamulid  22763  mamurid  22764  mat1dimid  22796  scmatf1  22853  mdetdiagid  22922  chpdmatlem3  23165  chpidmat  23172  fclscmpi  24355  ioorinv  25904  ig1pval2  26502  dgrcolem2  26600  plydivlem4  26624  vieta1lem2  26641  0cxp  27001  cxpexp  27003  lgs0  27644  lgs2  27648  2lgs2  27739  left1s  28288  exps0  28820  axlowdim  29546  1loopgrvd2  30091  eupth2  30847  ex-prmo  31067  madjusmdetlem1  34507  signsw0glem  35230  breprexp  35310  ex-sategoelel  36274  rdgprc0  36649  bj-pr11val  38012  bj-pr22val  38026  mapdhval0  42889  hdmap1val0  42963  refsum2cnlem1  46161  liminf10ex  46891  cncfiooicclem1  47010  fouriersw  47348  hspmbllem1  47743  blen0  49791  0dig1  49828  parhomid2  50858  parswapprop  50884  par2hom  50886