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 1541  ifcif 4528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-if 4529

This theorem is referenced by:  oe0m  8520  ttrcltr  9713  ttukeylem4  10509  xnegpnf  13190  xnegmnf  13191  xaddpnf1  13207  xaddpnf2  13208  xaddmnf1  13209  xaddmnf2  13210  pnfaddmnf  13211  mnfaddpnf  13212  xmul01  13248  exp0  14033  swrd00  14596  sgn0  15038  lcm0val  16533  prmo2  16975  prmo3  16976  prmo5  17064  mulg0  18959  zzngim  21114  obsipid  21283  mvrid  21549  mamulid  21950  mamurid  21951  mat1dimid  21983  scmatf1  22040  mdetdiagid  22109  chpdmatlem3  22349  chpidmat  22356  fclscmpi  23540  ioorinv  25100  ig1pval2  25698  dgrcolem2  25795  plydivlem4  25816  vieta1lem2  25831  0cxp  26181  cxpexp  26183  lgs0  26820  lgs2  26824  2lgs2  26915  left1s  27397  axlowdim  28257  1loopgrvd2  28798  eupth2  29530  ex-prmo  29750  madjusmdetlem1  32876  signsw0glem  33633  breprexp  33714  ex-sategoelel  34481  rdgprc0  34834  bj-pr11val  35972  bj-pr22val  35986  mapdhval0  40682  hdmap1val0  40756  refsum2cnlem1  43803  liminf10ex  44569  cncfiooicclem1  44688  fouriersw  45026  hspmbllem1  45421  blen0  47336  0dig1  47373