Theorem iftruei 4484

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

Syntax hints:   = wceq 1559  ifcif 4477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4478

This theorem is referenced by:  oe0m  8481  ttrcltr  9665  ttukeylem4  10463  xnegpnf  13206  xnegmnf  13207  xaddpnf1  13223  xaddpnf2  13224  xaddmnf1  13225  xaddmnf2  13226  pnfaddmnf  13227  mnfaddpnf  13228  xmul01  13264  exp0  14072  swrd00  14652  sgn0  15096  lcm0val  16619  prmo2  17067  prmo3  17068  prmo5  17156  mulg0  19107  zzngim  21592  obsipid  21762  mvrid  22023  mamulid  22489  mamurid  22490  mat1dimid  22522  scmatf1  22579  mdetdiagid  22648  chpdmatlem3  22888  chpidmat  22895  fclscmpi  24077  ioorinv  25626  ig1pval2  26225  dgrcolem2  26322  plydivlem4  26348  vieta1lem2  26363  0cxp  26719  cxpexp  26721  lgs0  27362  lgs2  27366  2lgs2  27457  left1s  27976  exps0  28508  axlowdim  29119  1loopgrvd2  29661  eupth2  30398  ex-prmo  30618  madjusmdetlem1  34085  signsw0glem  34808  breprexp  34888  ex-sategoelel  35732  rdgprc0  36102  bj-pr11val  37451  bj-pr22val  37465  mapdhval0  42310  hdmap1val0  42384  refsum2cnlem1  45578  liminf10ex  46309  cncfiooicclem1  46428  fouriersw  46766  hspmbllem1  47161  blen0  49155  0dig1  49192