Theorem iftruei 4474

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

Syntax hints:   = wceq 1533  ifcif 4467

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 4468

This theorem is referenced by:  oe0m  8137  ttukeylem4  9928  xnegpnf  12596  xnegmnf  12597  xaddpnf1  12613  xaddpnf2  12614  xaddmnf1  12615  xaddmnf2  12616  pnfaddmnf  12617  mnfaddpnf  12618  xmul01  12654  exp0  13427  swrd00  14000  sgn0  14442  lcm0val  15932  prmo2  16370  prmo3  16371  prmo5  16456  mulg0  18225  mvrid  20197  zzngim  20693  obsipid  20860  mamulid  21044  mamurid  21045  mat1dimid  21077  scmatf1  21134  mdetdiagid  21203  chpdmatlem3  21442  chpidmat  21449  fclscmpi  22631  ioorinv  24171  ig1pval2  24761  dgrcolem2  24858  plydivlem4  24879  vieta1lem2  24894  0cxp  25243  cxpexp  25245  lgs0  25880  lgs2  25884  2lgs2  25975  axlowdim  26741  1loopgrvd2  27279  eupth2  28012  ex-prmo  28232  madjusmdetlem1  31087  signsw0glem  31818  breprexp  31899  ex-sategoelel  32663  rdgprc0  33033  bj-pr11val  34312  bj-pr22val  34326  mapdhval0  38855  hdmap1val0  38929  refsum2cnlem1  41287  liminf10ex  42047  cncfiooicclem1  42168  fouriersw  42509  hspmbllem1  42901  blen0  44625  0dig1  44662