Theorem iftruei 4461

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

Syntax hints:   = wceq 1547  ifcif 4454

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 4455

This theorem is referenced by:  oe0m  8443  ttrcltr  9628  ttukeylem4  10425  xnegpnf  13152  xnegmnf  13153  xaddpnf1  13169  xaddpnf2  13170  xaddmnf1  13171  xaddmnf2  13172  pnfaddmnf  13173  mnfaddpnf  13174  xmul01  13210  exp0  14018  swrd00  14598  sgn0  15042  lcm0val  16554  prmo2  17002  prmo3  17003  prmo5  17090  mulg0  19041  zzngim  21527  obsipid  21697  mvrid  21958  mamulid  22424  mamurid  22425  mat1dimid  22457  scmatf1  22514  mdetdiagid  22583  chpdmatlem3  22823  chpidmat  22830  fclscmpi  24012  ioorinv  25561  ig1pval2  26160  dgrcolem2  26257  plydivlem4  26280  vieta1lem2  26295  0cxp  26648  cxpexp  26650  lgs0  27291  lgs2  27295  2lgs2  27386  left1s  27905  exps0  28437  axlowdim  29048  1loopgrvd2  29590  eupth2  30327  ex-prmo  30547  madjusmdetlem1  34011  signsw0glem  34737  breprexp  34817  ex-sategoelel  35649  rdgprc0  36019  bj-pr11val  37358  bj-pr22val  37372  mapdhval0  42217  hdmap1val0  42291  refsum2cnlem1  45485  liminf10ex  46217  cncfiooicclem1  46336  fouriersw  46674  hspmbllem1  47069  blen0  49063  0dig1  49100