Theorem iftruei 4499

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

Syntax hints:   = wceq 1567  ifcif 4492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-if 4493

This theorem is referenced by:  oe0m  8502  ttrcltr  9684  ttukeylem4  10495  xnegpnf  13234  xnegmnf  13235  xaddpnf1  13251  xaddpnf2  13252  xaddmnf1  13253  xaddmnf2  13254  pnfaddmnf  13255  mnfaddpnf  13256  xmul01  13292  exp0  14100  swrd00  14681  sgn0  15125  lcm0val  16651  prmo2  17099  prmo3  17100  prmo5  17188  mulg0  19139  zzngim  21670  obsipid  21840  mvrid  22101  mamulid  22566  mamurid  22567  mat1dimid  22599  scmatf1  22656  mdetdiagid  22725  chpdmatlem3  22965  chpidmat  22972  fclscmpi  24154  ioorinv  25703  ig1pval2  26302  dgrcolem2  26399  plydivlem4  26425  vieta1lem2  26440  0cxp  26796  cxpexp  26798  lgs0  27439  lgs2  27443  2lgs2  27534  left1s  28053  exps0  28585  axlowdim  29251  1loopgrvd2  29793  eupth2  30530  ex-prmo  30750  madjusmdetlem1  34161  signsw0glem  34884  breprexp  34964  ex-sategoelel  35811  rdgprc0  36181  bj-pr11val  37528  bj-pr22val  37542  mapdhval0  42388  hdmap1val0  42462  refsum2cnlem1  45648  liminf10ex  46379  cncfiooicclem1  46498  fouriersw  46836  hspmbllem1  47231  blen0  49236  0dig1  49273