Theorem iftruei 4498

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

Syntax hints:   = wceq 1540  ifcif 4491

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4492

This theorem is referenced by:  oe0m  8485  ttrcltr  9676  ttukeylem4  10472  xnegpnf  13176  xnegmnf  13177  xaddpnf1  13193  xaddpnf2  13194  xaddmnf1  13195  xaddmnf2  13196  pnfaddmnf  13197  mnfaddpnf  13198  xmul01  13234  exp0  14037  swrd00  14616  sgn0  15062  lcm0val  16571  prmo2  17018  prmo3  17019  prmo5  17106  mulg0  19013  zzngim  21469  obsipid  21638  mvrid  21900  mamulid  22335  mamurid  22336  mat1dimid  22368  scmatf1  22425  mdetdiagid  22494  chpdmatlem3  22734  chpidmat  22741  fclscmpi  23923  ioorinv  25484  ig1pval2  26089  dgrcolem2  26187  plydivlem4  26211  vieta1lem2  26226  0cxp  26582  cxpexp  26584  lgs0  27228  lgs2  27232  2lgs2  27323  left1s  27813  exps0  28320  axlowdim  28895  1loopgrvd2  29438  eupth2  30175  ex-prmo  30395  madjusmdetlem1  33824  signsw0glem  34551  breprexp  34631  ex-sategoelel  35415  rdgprc0  35788  bj-pr11val  37000  bj-pr22val  37014  mapdhval0  41726  hdmap1val0  41800  refsum2cnlem1  45038  liminf10ex  45779  cncfiooicclem1  45898  fouriersw  46236  hspmbllem1  46631  blen0  48565  0dig1  48602