Theorem iftruei 4471

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

Syntax hints:   = wceq 1541  ifcif 4464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-if 4465

This theorem is referenced by:  oe0m  8324  ttrcltr  9435  ttukeylem4  10252  xnegpnf  12925  xnegmnf  12926  xaddpnf1  12942  xaddpnf2  12943  xaddmnf1  12944  xaddmnf2  12945  pnfaddmnf  12946  mnfaddpnf  12947  xmul01  12983  exp0  13767  swrd00  14338  sgn0  14781  lcm0val  16280  prmo2  16722  prmo3  16723  prmo5  16811  mulg0  18688  zzngim  20741  obsipid  20910  mvrid  21173  mamulid  21571  mamurid  21572  mat1dimid  21604  scmatf1  21661  mdetdiagid  21730  chpdmatlem3  21970  chpidmat  21977  fclscmpi  23161  ioorinv  24721  ig1pval2  25319  dgrcolem2  25416  plydivlem4  25437  vieta1lem2  25452  0cxp  25802  cxpexp  25804  lgs0  26439  lgs2  26443  2lgs2  26534  axlowdim  27310  1loopgrvd2  27851  eupth2  28582  ex-prmo  28802  madjusmdetlem1  31756  signsw0glem  32511  breprexp  32592  ex-sategoelel  33362  rdgprc0  33748  bj-pr11val  35174  bj-pr22val  35188  mapdhval0  39718  hdmap1val0  39792  refsum2cnlem1  42533  liminf10ex  43269  cncfiooicclem1  43388  fouriersw  43726  hspmbllem1  44118  blen0  45870  0dig1  45907