Theorem iftruei 4496

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

This proof depends on syntax axioms:   = wceq 1570  ifcif 4489

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4490

This theorem is used by:  oe0m  8509  ttrcltr  9692  ttukeylem4  10511  xnegpnf  13251  xnegmnf  13252  xaddpnf1  13268  xaddpnf2  13269  xaddmnf1  13270  xaddmnf2  13271  pnfaddmnf  13272  mnfaddpnf  13273  xmul01  13309  exp0  14119  swrd00  14702  sgn0  15150  lcm0val  16674  prmo2  17122  prmo3  17123  prmo5  17211  mulg0  19184  zzngim  21752  obsipid  21922  mvrid  22183  mamulid  22648  mamurid  22649  mat1dimid  22681  scmatf1  22738  mdetdiagid  22807  chpdmatlem3  23047  chpidmat  23054  fclscmpi  24237  ioorinv  25786  ig1pval2  26385  dgrcolem2  26482  plydivlem4  26508  vieta1lem2  26523  0cxp  26882  cxpexp  26884  lgs0  27525  lgs2  27529  2lgs2  27620  left1s  28139  exps0  28671  axlowdim  29366  1loopgrvd2  29911  eupth2  30661  ex-prmo  30881  madjusmdetlem1  34281  signsw0glem  35005  breprexp  35085  ex-sategoelel  35950  rdgprc0  36320  bj-pr11val  37698  bj-pr22val  37712  mapdhval0  42557  hdmap1val0  42631  refsum2cnlem1  45815  liminf10ex  46546  cncfiooicclem1  46665  fouriersw  47003  hspmbllem1  47398  blen0  49409  0dig1  49446