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(𝜑, 𝐴, 𝐵) = 𝐴

Syntax hints:   = wceq 1542  ifcif 4481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4482

This theorem is referenced by:  oe0m  8455  ttrcltr  9637  ttukeylem4  10434  xnegpnf  13136  xnegmnf  13137  xaddpnf1  13153  xaddpnf2  13154  xaddmnf1  13155  xaddmnf2  13156  pnfaddmnf  13157  mnfaddpnf  13158  xmul01  13194  exp0  14000  swrd00  14580  sgn0  15024  lcm0val  16533  prmo2  16980  prmo3  16981  prmo5  17068  mulg0  19016  zzngim  21519  obsipid  21689  mvrid  21951  mamulid  22397  mamurid  22398  mat1dimid  22430  scmatf1  22487  mdetdiagid  22556  chpdmatlem3  22796  chpidmat  22803  fclscmpi  23985  ioorinv  25545  ig1pval2  26150  dgrcolem2  26248  plydivlem4  26272  vieta1lem2  26287  0cxp  26643  cxpexp  26645  lgs0  27289  lgs2  27293  2lgs2  27384  left1s  27903  exps0  28435  axlowdim  29046  1loopgrvd2  29589  eupth2  30326  ex-prmo  30546  madjusmdetlem1  34005  signsw0glem  34731  breprexp  34811  ex-sategoelel  35637  rdgprc0  36007  bj-pr11val  37253  bj-pr22val  37267  mapdhval0  42101  hdmap1val0  42175  refsum2cnlem1  45397  liminf10ex  46132  cncfiooicclem1  46251  fouriersw  46589  hspmbllem1  46984  blen0  48932  0dig1  48969