Theorem iftruei 4432

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

Syntax hints:   = wceq 1543  ifcif 4425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-if 4426

This theorem is referenced by:  oe0m  8223  ttukeylem4  10091  xnegpnf  12764  xnegmnf  12765  xaddpnf1  12781  xaddpnf2  12782  xaddmnf1  12783  xaddmnf2  12784  pnfaddmnf  12785  mnfaddpnf  12786  xmul01  12822  exp0  13604  swrd00  14174  sgn0  14617  lcm0val  16114  prmo2  16556  prmo3  16557  prmo5  16645  mulg0  18449  zzngim  20471  obsipid  20638  mvrid  20902  mamulid  21292  mamurid  21293  mat1dimid  21325  scmatf1  21382  mdetdiagid  21451  chpdmatlem3  21691  chpidmat  21698  fclscmpi  22880  ioorinv  24427  ig1pval2  25025  dgrcolem2  25122  plydivlem4  25143  vieta1lem2  25158  0cxp  25508  cxpexp  25510  lgs0  26145  lgs2  26149  2lgs2  26240  axlowdim  27006  1loopgrvd2  27545  eupth2  28276  ex-prmo  28496  madjusmdetlem1  31445  signsw0glem  32198  breprexp  32279  ex-sategoelel  33050  rdgprc0  33439  bj-pr11val  34881  bj-pr22val  34895  mapdhval0  39425  hdmap1val0  39499  refsum2cnlem1  42194  liminf10ex  42933  cncfiooicclem1  43052  fouriersw  43390  hspmbllem1  43782  blen0  45534  0dig1  45571