Theorem iftruei 4491

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

Syntax hints:   = wceq 1540  ifcif 4484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4485

This theorem is referenced by:  oe0m  8459  ttrcltr  9645  ttukeylem4  10441  xnegpnf  13145  xnegmnf  13146  xaddpnf1  13162  xaddpnf2  13163  xaddmnf1  13164  xaddmnf2  13165  pnfaddmnf  13166  mnfaddpnf  13167  xmul01  13203  exp0  14006  swrd00  14585  sgn0  15031  lcm0val  16540  prmo2  16987  prmo3  16988  prmo5  17075  mulg0  18982  zzngim  21438  obsipid  21607  mvrid  21869  mamulid  22304  mamurid  22305  mat1dimid  22337  scmatf1  22394  mdetdiagid  22463  chpdmatlem3  22703  chpidmat  22710  fclscmpi  23892  ioorinv  25453  ig1pval2  26058  dgrcolem2  26156  plydivlem4  26180  vieta1lem2  26195  0cxp  26551  cxpexp  26553  lgs0  27197  lgs2  27201  2lgs2  27292  left1s  27782  exps0  28289  axlowdim  28864  1loopgrvd2  29407  eupth2  30141  ex-prmo  30361  madjusmdetlem1  33790  signsw0glem  34517  breprexp  34597  ex-sategoelel  35381  rdgprc0  35754  bj-pr11val  36966  bj-pr22val  36980  mapdhval0  41692  hdmap1val0  41766  refsum2cnlem1  45004  liminf10ex  45745  cncfiooicclem1  45864  fouriersw  46202  hspmbllem1  46597  blen0  48534  0dig1  48571