Theorem iftruei 4486

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

Syntax hints:   = wceq 1541  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4480

This theorem is referenced by:  oe0m  8445  ttrcltr  9625  ttukeylem4  10422  xnegpnf  13124  xnegmnf  13125  xaddpnf1  13141  xaddpnf2  13142  xaddmnf1  13143  xaddmnf2  13144  pnfaddmnf  13145  mnfaddpnf  13146  xmul01  13182  exp0  13988  swrd00  14568  sgn0  15012  lcm0val  16521  prmo2  16968  prmo3  16969  prmo5  17056  mulg0  19004  zzngim  21507  obsipid  21677  mvrid  21939  mamulid  22385  mamurid  22386  mat1dimid  22418  scmatf1  22475  mdetdiagid  22544  chpdmatlem3  22784  chpidmat  22791  fclscmpi  23973  ioorinv  25533  ig1pval2  26138  dgrcolem2  26236  plydivlem4  26260  vieta1lem2  26275  0cxp  26631  cxpexp  26633  lgs0  27277  lgs2  27281  2lgs2  27372  left1s  27891  exps0  28423  axlowdim  29034  1loopgrvd2  29577  eupth2  30314  ex-prmo  30534  madjusmdetlem1  33984  signsw0glem  34710  breprexp  34790  ex-sategoelel  35615  rdgprc0  35985  bj-pr11val  37206  bj-pr22val  37220  mapdhval0  41985  hdmap1val0  42059  refsum2cnlem1  45282  liminf10ex  46018  cncfiooicclem1  46137  fouriersw  46475  hspmbllem1  46870  blen0  48818  0dig1  48855