Theorem iftruei 4494

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

Syntax hints:   = wceq 1570  ifcif 4487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-if 4488

This theorem is referenced by:  oe0m  8499  ttrcltr  9681  ttukeylem4  10491  xnegpnf  13230  xnegmnf  13231  xaddpnf1  13247  xaddpnf2  13248  xaddmnf1  13249  xaddmnf2  13250  pnfaddmnf  13251  mnfaddpnf  13252  xmul01  13288  exp0  14097  swrd00  14678  sgn0  15122  lcm0val  16647  prmo2  17095  prmo3  17096  prmo5  17184  mulg0  19135  zzngim  21702  obsipid  21872  mvrid  22133  mamulid  22598  mamurid  22599  mat1dimid  22631  scmatf1  22688  mdetdiagid  22757  chpdmatlem3  22997  chpidmat  23004  fclscmpi  24186  ioorinv  25735  ig1pval2  26334  dgrcolem2  26431  plydivlem4  26457  vieta1lem2  26472  0cxp  26831  cxpexp  26833  lgs0  27474  lgs2  27478  2lgs2  27569  left1s  28088  exps0  28620  axlowdim  29311  1loopgrvd2  29853  eupth2  30590  ex-prmo  30810  madjusmdetlem1  34217  signsw0glem  34940  breprexp  35020  ex-sategoelel  35913  rdgprc0  36283  bj-pr11val  37641  bj-pr22val  37655  mapdhval0  42499  hdmap1val0  42573  refsum2cnlem1  45757  liminf10ex  46488  cncfiooicclem1  46607  fouriersw  46945  hspmbllem1  47340  blen0  49352  0dig1  49389