Theorem iftruei 4477

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

Syntax hints:   = wceq 1541  ifcif 4470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-if 4471

This theorem is referenced by:  oe0m  8428  ttrcltr  9601  ttukeylem4  10398  xnegpnf  13103  xnegmnf  13104  xaddpnf1  13120  xaddpnf2  13121  xaddmnf1  13122  xaddmnf2  13123  pnfaddmnf  13124  mnfaddpnf  13125  xmul01  13161  exp0  13967  swrd00  14547  sgn0  14991  lcm0val  16500  prmo2  16947  prmo3  16948  prmo5  17035  mulg0  18982  zzngim  21484  obsipid  21654  mvrid  21916  mamulid  22351  mamurid  22352  mat1dimid  22384  scmatf1  22441  mdetdiagid  22510  chpdmatlem3  22750  chpidmat  22757  fclscmpi  23939  ioorinv  25499  ig1pval2  26104  dgrcolem2  26202  plydivlem4  26226  vieta1lem2  26241  0cxp  26597  cxpexp  26599  lgs0  27243  lgs2  27247  2lgs2  27338  left1s  27835  exps0  28345  axlowdim  28934  1loopgrvd2  29477  eupth2  30211  ex-prmo  30431  madjusmdetlem1  33832  signsw0glem  34558  breprexp  34638  ex-sategoelel  35457  rdgprc0  35827  bj-pr11val  37039  bj-pr22val  37053  mapdhval0  41764  hdmap1val0  41838  refsum2cnlem1  45074  liminf10ex  45812  cncfiooicclem1  45931  fouriersw  46269  hspmbllem1  46664  blen0  48604  0dig1  48641