Theorem iftruei 4043

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

Syntax hints:   = wceq 1475  ifcif 4036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037

This theorem is referenced by:  oe0m  7485  ttukeylem4  9217  xnegpnf  11914  xnegmnf  11915  xaddpnf1  11931  xaddpnf2  11932  xaddmnf1  11933  xaddmnf2  11934  pnfaddmnf  11935  mnfaddpnf  11936  xmul01  11969  exp0  12726  swrd00  13270  sgn0  13677  lcm0val  15145  prmo2  15582  prmo3  15583  prmo5  15674  mulg0  17369  mvrid  19244  zzngim  19720  obsipid  19885  mamulid  20066  mamurid  20067  mat1dimid  20099  scmatf1  20156  mdetdiagid  20225  chpdmatlem3  20464  chpidmat  20471  fclscmpi  21643  ioorinv  23150  ig1pval2  23737  dgrcolem2  23834  plydivlem4  23855  vieta1lem2  23870  0cxp  24212  cxpexp  24214  lgs0  24835  lgs2  24839  2lgs2  24930  axlowdim  25641  vtxvalsnop  25716  iedgvalsnop  25717  ex-prmo  26708  madjusmdetlem1  29221  signsw0glem  29956  rdgprc0  30943  bj-pr11val  32186  bj-pr22val  32200  mapdhval0  36032  hdmap1val0  36107  refsum2cnlem1  38219  cncfiooicclem1  38779  fouriersw  39124  hspmbllem1  39516  1loopgrvd2  40718  eupth2  41407  blen0  42164  0dig1  42201