Theorem iftruei 4507

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

Syntax hints:   = wceq 1540  ifcif 4500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-if 4501

This theorem is referenced by:  oe0m  8530  ttrcltr  9730  ttukeylem4  10526  xnegpnf  13225  xnegmnf  13226  xaddpnf1  13242  xaddpnf2  13243  xaddmnf1  13244  xaddmnf2  13245  pnfaddmnf  13246  mnfaddpnf  13247  xmul01  13283  exp0  14083  swrd00  14662  sgn0  15108  lcm0val  16613  prmo2  17060  prmo3  17061  prmo5  17148  mulg0  19057  zzngim  21513  obsipid  21682  mvrid  21944  mamulid  22379  mamurid  22380  mat1dimid  22412  scmatf1  22469  mdetdiagid  22538  chpdmatlem3  22778  chpidmat  22785  fclscmpi  23967  ioorinv  25529  ig1pval2  26134  dgrcolem2  26232  plydivlem4  26256  vieta1lem2  26271  0cxp  26627  cxpexp  26629  lgs0  27273  lgs2  27277  2lgs2  27368  left1s  27858  exps0  28365  axlowdim  28940  1loopgrvd2  29483  eupth2  30220  ex-prmo  30440  madjusmdetlem1  33858  signsw0glem  34585  breprexp  34665  ex-sategoelel  35443  rdgprc0  35811  bj-pr11val  37023  bj-pr22val  37037  mapdhval0  41744  hdmap1val0  41818  refsum2cnlem1  45061  liminf10ex  45803  cncfiooicclem1  45922  fouriersw  46260  hspmbllem1  46655  blen0  48552  0dig1  48589