Theorem iftruei 4473

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

Syntax hints:   = wceq 1533  ifcif 4466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-if 4467

This theorem is referenced by:  oe0m  8142  ttukeylem4  9933  xnegpnf  12601  xnegmnf  12602  xaddpnf1  12618  xaddpnf2  12619  xaddmnf1  12620  xaddmnf2  12621  pnfaddmnf  12622  mnfaddpnf  12623  xmul01  12659  exp0  13432  swrd00  14005  sgn0  14447  lcm0val  15937  prmo2  16375  prmo3  16376  prmo5  16461  mulg0  18230  mvrid  20202  zzngim  20698  obsipid  20865  mamulid  21049  mamurid  21050  mat1dimid  21082  scmatf1  21139  mdetdiagid  21208  chpdmatlem3  21447  chpidmat  21454  fclscmpi  22636  ioorinv  24176  ig1pval2  24766  dgrcolem2  24863  plydivlem4  24884  vieta1lem2  24899  0cxp  25248  cxpexp  25250  lgs0  25885  lgs2  25889  2lgs2  25980  axlowdim  26746  1loopgrvd2  27284  eupth2  28017  ex-prmo  28237  madjusmdetlem1  31092  signsw0glem  31823  breprexp  31904  ex-sategoelel  32668  rdgprc0  33038  bj-pr11val  34317  bj-pr22val  34331  mapdhval0  38860  hdmap1val0  38934  refsum2cnlem1  41292  liminf10ex  42053  cncfiooicclem1  42174  fouriersw  42515  hspmbllem1  42907  blen0  44631  0dig1  44668