Theorem iftruei 4473

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

Syntax hints:   = wceq 1542  ifcif 4466

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4467

This theorem is referenced by:  oe0m  8453  ttrcltr  9637  ttukeylem4  10434  xnegpnf  13161  xnegmnf  13162  xaddpnf1  13178  xaddpnf2  13179  xaddmnf1  13180  xaddmnf2  13181  pnfaddmnf  13182  mnfaddpnf  13183  xmul01  13219  exp0  14027  swrd00  14607  sgn0  15051  lcm0val  16563  prmo2  17011  prmo3  17012  prmo5  17099  mulg0  19050  zzngim  21532  obsipid  21702  mvrid  21962  mamulid  22406  mamurid  22407  mat1dimid  22439  scmatf1  22496  mdetdiagid  22565  chpdmatlem3  22805  chpidmat  22812  fclscmpi  23994  ioorinv  25543  ig1pval2  26142  dgrcolem2  26239  plydivlem4  26262  vieta1lem2  26277  0cxp  26630  cxpexp  26632  lgs0  27273  lgs2  27277  2lgs2  27368  left1s  27887  exps0  28419  axlowdim  29030  1loopgrvd2  29572  eupth2  30309  ex-prmo  30529  madjusmdetlem1  33971  signsw0glem  34697  breprexp  34777  ex-sategoelel  35603  rdgprc0  35973  bj-pr11val  37312  bj-pr22val  37326  mapdhval0  42171  hdmap1val0  42245  refsum2cnlem1  45468  liminf10ex  46202  cncfiooicclem1  46321  fouriersw  46659  hspmbllem1  47054  blen0  49048  0dig1  49085