Theorem iftruei 4532

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

Syntax hints:   = wceq 1540  ifcif 4525

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4526

This theorem is referenced by:  oe0m  8556  ttrcltr  9756  ttukeylem4  10552  xnegpnf  13251  xnegmnf  13252  xaddpnf1  13268  xaddpnf2  13269  xaddmnf1  13270  xaddmnf2  13271  pnfaddmnf  13272  mnfaddpnf  13273  xmul01  13309  exp0  14106  swrd00  14682  sgn0  15128  lcm0val  16631  prmo2  17078  prmo3  17079  prmo5  17166  mulg0  19092  zzngim  21571  obsipid  21742  mvrid  22004  mamulid  22447  mamurid  22448  mat1dimid  22480  scmatf1  22537  mdetdiagid  22606  chpdmatlem3  22846  chpidmat  22853  fclscmpi  24037  ioorinv  25611  ig1pval2  26216  dgrcolem2  26314  plydivlem4  26338  vieta1lem2  26353  0cxp  26708  cxpexp  26710  lgs0  27354  lgs2  27358  2lgs2  27449  left1s  27933  exps0  28410  axlowdim  28976  1loopgrvd2  29521  eupth2  30258  ex-prmo  30478  madjusmdetlem1  33826  signsw0glem  34568  breprexp  34648  ex-sategoelel  35426  rdgprc0  35794  bj-pr11val  37006  bj-pr22val  37020  mapdhval0  41727  hdmap1val0  41801  refsum2cnlem1  45042  liminf10ex  45789  cncfiooicclem1  45908  fouriersw  46246  hspmbllem1  46641  blen0  48493  0dig1  48530