Theorem iftruei 4474

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

Syntax hints:   = wceq 1542  ifcif 4467

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 4468

This theorem is referenced by:  oe0m  8446  ttrcltr  9628  ttukeylem4  10425  xnegpnf  13152  xnegmnf  13153  xaddpnf1  13169  xaddpnf2  13170  xaddmnf1  13171  xaddmnf2  13172  pnfaddmnf  13173  mnfaddpnf  13174  xmul01  13210  exp0  14018  swrd00  14598  sgn0  15042  lcm0val  16554  prmo2  17002  prmo3  17003  prmo5  17090  mulg0  19041  zzngim  21542  obsipid  21712  mvrid  21972  mamulid  22416  mamurid  22417  mat1dimid  22449  scmatf1  22506  mdetdiagid  22575  chpdmatlem3  22815  chpidmat  22822  fclscmpi  24004  ioorinv  25553  ig1pval2  26152  dgrcolem2  26249  plydivlem4  26273  vieta1lem2  26288  0cxp  26643  cxpexp  26645  lgs0  27287  lgs2  27291  2lgs2  27382  left1s  27901  exps0  28433  axlowdim  29044  1loopgrvd2  29587  eupth2  30324  ex-prmo  30544  madjusmdetlem1  33987  signsw0glem  34713  breprexp  34793  ex-sategoelel  35619  rdgprc0  35989  bj-pr11val  37328  bj-pr22val  37342  mapdhval0  42185  hdmap1val0  42259  refsum2cnlem1  45486  liminf10ex  46220  cncfiooicclem1  46339  fouriersw  46677  hspmbllem1  47072  blen0  49060  0dig1  49097