Theorem iftruei 4472

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

Syntax hints:   = wceq 1539  ifcif 4465

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-if 4466

This theorem is referenced by:  oe0m  8379  ttrcltr  9518  ttukeylem4  10314  xnegpnf  12989  xnegmnf  12990  xaddpnf1  13006  xaddpnf2  13007  xaddmnf1  13008  xaddmnf2  13009  pnfaddmnf  13010  mnfaddpnf  13011  xmul01  13047  exp0  13832  swrd00  14402  sgn0  14845  lcm0val  16344  prmo2  16786  prmo3  16787  prmo5  16875  mulg0  18752  zzngim  20805  obsipid  20974  mvrid  21237  mamulid  21635  mamurid  21636  mat1dimid  21668  scmatf1  21725  mdetdiagid  21794  chpdmatlem3  22034  chpidmat  22041  fclscmpi  23225  ioorinv  24785  ig1pval2  25383  dgrcolem2  25480  plydivlem4  25501  vieta1lem2  25516  0cxp  25866  cxpexp  25868  lgs0  26503  lgs2  26507  2lgs2  26598  axlowdim  27374  1loopgrvd2  27915  eupth2  28648  ex-prmo  28868  madjusmdetlem1  31822  signsw0glem  32577  breprexp  32658  ex-sategoelel  33428  rdgprc0  33814  bj-pr11val  35239  bj-pr22val  35253  mapdhval0  39781  hdmap1val0  39855  refsum2cnlem1  42618  liminf10ex  43364  cncfiooicclem1  43483  fouriersw  43821  hspmbllem1  44214  blen0  45976  0dig1  46013