Theorem iftruei 4388

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

Syntax hints:   = wceq 1522  ifcif 4381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-ex 1762  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-if 4382

This theorem is referenced by:  oe0m  7994  ttukeylem4  9780  xnegpnf  12452  xnegmnf  12453  xaddpnf1  12469  xaddpnf2  12470  xaddmnf1  12471  xaddmnf2  12472  pnfaddmnf  12473  mnfaddpnf  12474  xmul01  12510  exp0  13283  swrd00  13842  sgn0  14282  lcm0val  15767  prmo2  16205  prmo3  16206  prmo5  16291  mulg0  17988  mvrid  19891  zzngim  20381  obsipid  20548  mamulid  20734  mamurid  20735  mat1dimid  20767  scmatf1  20824  mdetdiagid  20893  chpdmatlem3  21132  chpidmat  21139  fclscmpi  22321  ioorinv  23860  ig1pval2  24450  dgrcolem2  24547  plydivlem4  24568  vieta1lem2  24583  0cxp  24930  cxpexp  24932  lgs0  25568  lgs2  25572  2lgs2  25663  axlowdim  26430  1loopgrvd2  26968  eupth2  27706  ex-prmo  27930  madjusmdetlem1  30707  signsw0glem  31440  breprexp  31521  ex-sategoelel  32276  rdgprc0  32647  bj-pr11val  33922  bj-pr22val  33936  mapdhval0  38392  hdmap1val0  38466  refsum2cnlem1  40833  liminf10ex  41597  cncfiooicclem1  41717  fouriersw  42058  hspmbllem1  42450  blen0  44113  0dig1  44150