Theorem iftruei 4535

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

Syntax hints:   = wceq 1542  ifcif 4528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4529

This theorem is referenced by:  oe0m  8515  ttrcltr  9708  ttukeylem4  10504  xnegpnf  13185  xnegmnf  13186  xaddpnf1  13202  xaddpnf2  13203  xaddmnf1  13204  xaddmnf2  13205  pnfaddmnf  13206  mnfaddpnf  13207  xmul01  13243  exp0  14028  swrd00  14591  sgn0  15033  lcm0val  16528  prmo2  16970  prmo3  16971  prmo5  17059  mulg0  18952  zzngim  21100  obsipid  21269  mvrid  21535  mamulid  21935  mamurid  21936  mat1dimid  21968  scmatf1  22025  mdetdiagid  22094  chpdmatlem3  22334  chpidmat  22341  fclscmpi  23525  ioorinv  25085  ig1pval2  25683  dgrcolem2  25780  plydivlem4  25801  vieta1lem2  25816  0cxp  26166  cxpexp  26168  lgs0  26803  lgs2  26807  2lgs2  26898  left1s  27379  axlowdim  28209  1loopgrvd2  28750  eupth2  29482  ex-prmo  29702  madjusmdetlem1  32796  signsw0glem  33553  breprexp  33634  ex-sategoelel  34401  rdgprc0  34754  bj-pr11val  35875  bj-pr22val  35889  mapdhval0  40585  hdmap1val0  40659  refsum2cnlem1  43707  liminf10ex  44477  cncfiooicclem1  44596  fouriersw  44934  hspmbllem1  45329  blen0  47212  0dig1  47249