Theorem iftruei 4462

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

Syntax hints:   = wceq 1547  ifcif 4455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-if 4456

This theorem is referenced by:  oe0m  8444  ttrcltr  9629  ttukeylem4  10426  xnegpnf  13153  xnegmnf  13154  xaddpnf1  13170  xaddpnf2  13171  xaddmnf1  13172  xaddmnf2  13173  pnfaddmnf  13174  mnfaddpnf  13175  xmul01  13211  exp0  14019  swrd00  14599  sgn0  15043  lcm0val  16555  prmo2  17003  prmo3  17004  prmo5  17091  mulg0  19042  zzngim  21528  obsipid  21698  mvrid  21959  mamulid  22425  mamurid  22426  mat1dimid  22458  scmatf1  22515  mdetdiagid  22584  chpdmatlem3  22824  chpidmat  22831  fclscmpi  24013  ioorinv  25562  ig1pval2  26161  dgrcolem2  26258  plydivlem4  26281  vieta1lem2  26296  0cxp  26649  cxpexp  26651  lgs0  27292  lgs2  27296  2lgs2  27387  left1s  27906  exps0  28438  axlowdim  29049  1loopgrvd2  29591  eupth2  30328  ex-prmo  30548  madjusmdetlem1  34020  signsw0glem  34746  breprexp  34826  ex-sategoelel  35658  rdgprc0  36028  bj-pr11val  37367  bj-pr22val  37381  mapdhval0  42226  hdmap1val0  42300  refsum2cnlem1  45494  liminf10ex  46225  cncfiooicclem1  46344  fouriersw  46682  hspmbllem1  47077  blen0  49071  0dig1  49108