Theorem iftruei 4495

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

Syntax hints:   = wceq 1540  ifcif 4488

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4489

This theorem is referenced by:  oe0m  8482  ttrcltr  9669  ttukeylem4  10465  xnegpnf  13169  xnegmnf  13170  xaddpnf1  13186  xaddpnf2  13187  xaddmnf1  13188  xaddmnf2  13189  pnfaddmnf  13190  mnfaddpnf  13191  xmul01  13227  exp0  14030  swrd00  14609  sgn0  15055  lcm0val  16564  prmo2  17011  prmo3  17012  prmo5  17099  mulg0  19006  zzngim  21462  obsipid  21631  mvrid  21893  mamulid  22328  mamurid  22329  mat1dimid  22361  scmatf1  22418  mdetdiagid  22487  chpdmatlem3  22727  chpidmat  22734  fclscmpi  23916  ioorinv  25477  ig1pval2  26082  dgrcolem2  26180  plydivlem4  26204  vieta1lem2  26219  0cxp  26575  cxpexp  26577  lgs0  27221  lgs2  27225  2lgs2  27316  left1s  27806  exps0  28313  axlowdim  28888  1loopgrvd2  29431  eupth2  30168  ex-prmo  30388  madjusmdetlem1  33817  signsw0glem  34544  breprexp  34624  ex-sategoelel  35408  rdgprc0  35781  bj-pr11val  36993  bj-pr22val  37007  mapdhval0  41719  hdmap1val0  41793  refsum2cnlem1  45031  liminf10ex  45772  cncfiooicclem1  45891  fouriersw  46229  hspmbllem1  46624  blen0  48561  0dig1  48598