Theorem iftruei 4483

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

Syntax hints:   = wceq 1540  ifcif 4476

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4477

This theorem is referenced by:  oe0m  8436  ttrcltr  9612  ttukeylem4  10406  xnegpnf  13111  xnegmnf  13112  xaddpnf1  13128  xaddpnf2  13129  xaddmnf1  13130  xaddmnf2  13131  pnfaddmnf  13132  mnfaddpnf  13133  xmul01  13169  exp0  13972  swrd00  14551  sgn0  14996  lcm0val  16505  prmo2  16952  prmo3  16953  prmo5  17040  mulg0  18953  zzngim  21459  obsipid  21629  mvrid  21891  mamulid  22326  mamurid  22327  mat1dimid  22359  scmatf1  22416  mdetdiagid  22485  chpdmatlem3  22725  chpidmat  22732  fclscmpi  23914  ioorinv  25475  ig1pval2  26080  dgrcolem2  26178  plydivlem4  26202  vieta1lem2  26217  0cxp  26573  cxpexp  26575  lgs0  27219  lgs2  27223  2lgs2  27314  left1s  27809  exps0  28319  axlowdim  28906  1loopgrvd2  29449  eupth2  30183  ex-prmo  30403  madjusmdetlem1  33794  signsw0glem  34521  breprexp  34601  ex-sategoelel  35394  rdgprc0  35767  bj-pr11val  36979  bj-pr22val  36993  mapdhval0  41704  hdmap1val0  41778  refsum2cnlem1  45015  liminf10ex  45755  cncfiooicclem1  45874  fouriersw  46212  hspmbllem1  46607  blen0  48557  0dig1  48594