Theorem iftruei 4492

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-if 4486

This theorem is used by:  oe0m  8564  ttrcltr  9754  ttukeylem4  10629  xnegpnf  13379  xnegmnf  13380  xaddpnf1  13396  xaddpnf2  13397  xaddmnf1  13398  xaddmnf2  13399  pnfaddmnf  13400  mnfaddpnf  13401  xmul01  13437  exp0  14248  swrd00  14834  sgn0  15285  lcm0val  16813  prmo2  17262  prmo3  17263  prmo5  17351  mulg0  19334  zzngim  21913  obsipid  22083  mvrid  22346  mamulid  22811  mamurid  22812  mat1dimid  22844  scmatf1  22901  mdetdiagid  22970  chpdmatlem3  23213  chpidmat  23220  fclscmpi  24403  ioorinv  25952  ig1pval2  26550  dgrcolem2  26648  plydivlem4  26672  vieta1lem2  26689  0cxp  27051  cxpexp  27053  lgs0  27694  lgs2  27698  2lgs2  27789  left1s  28338  exps0  28870  axlowdim  29596  1loopgrvd2  30141  eupth2  30897  ex-prmo  31117  madjusmdetlem1  34570  signsw0glem  35293  breprexp  35373  ex-sategoelel  36394  rdgprc0  36770  bj-pr11val  38133  bj-pr22val  38147  mapdhval0  43048  hdmap1val0  43122  refsum2cnlem1  46328  liminf10ex  47057  cncfiooicclem1  47176  fouriersw  47514  hspmbllem1  47909  blen0  50015  0dig1  50052  parhomid2  51082  parswapprop  51108  par2hom  51110