Theorem iftruei 4483

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

Syntax hints:   = wceq 1541  ifcif 4476

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-if 4477

This theorem is referenced by:  oe0m  8442  ttrcltr  9617  ttukeylem4  10414  xnegpnf  13115  xnegmnf  13116  xaddpnf1  13132  xaddpnf2  13133  xaddmnf1  13134  xaddmnf2  13135  pnfaddmnf  13136  mnfaddpnf  13137  xmul01  13173  exp0  13979  swrd00  14559  sgn0  15003  lcm0val  16512  prmo2  16959  prmo3  16960  prmo5  17047  mulg0  18995  zzngim  21498  obsipid  21668  mvrid  21930  mamulid  22376  mamurid  22377  mat1dimid  22409  scmatf1  22466  mdetdiagid  22535  chpdmatlem3  22775  chpidmat  22782  fclscmpi  23964  ioorinv  25524  ig1pval2  26129  dgrcolem2  26227  plydivlem4  26251  vieta1lem2  26266  0cxp  26622  cxpexp  26624  lgs0  27268  lgs2  27272  2lgs2  27363  left1s  27860  exps0  28370  axlowdim  28960  1loopgrvd2  29503  eupth2  30240  ex-prmo  30460  madjusmdetlem1  33912  signsw0glem  34638  breprexp  34718  ex-sategoelel  35537  rdgprc0  35907  bj-pr11val  37122  bj-pr22val  37136  mapdhval0  41897  hdmap1val0  41971  refsum2cnlem1  45198  liminf10ex  45934  cncfiooicclem1  46053  fouriersw  46391  hspmbllem1  46786  blen0  48734  0dig1  48771