Theorem iftruei 4555

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

Syntax hints:   = wceq 1537  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-if 4549

This theorem is referenced by:  oe0m  8574  ttrcltr  9785  ttukeylem4  10581  xnegpnf  13271  xnegmnf  13272  xaddpnf1  13288  xaddpnf2  13289  xaddmnf1  13290  xaddmnf2  13291  pnfaddmnf  13292  mnfaddpnf  13293  xmul01  13329  exp0  14116  swrd00  14692  sgn0  15138  lcm0val  16641  prmo2  17087  prmo3  17088  prmo5  17176  mulg0  19114  zzngim  21594  obsipid  21765  mvrid  22027  mamulid  22468  mamurid  22469  mat1dimid  22501  scmatf1  22558  mdetdiagid  22627  chpdmatlem3  22867  chpidmat  22874  fclscmpi  24058  ioorinv  25630  ig1pval2  26236  dgrcolem2  26334  plydivlem4  26356  vieta1lem2  26371  0cxp  26726  cxpexp  26728  lgs0  27372  lgs2  27376  2lgs2  27467  left1s  27951  exps0  28428  axlowdim  28994  1loopgrvd2  29539  eupth2  30271  ex-prmo  30491  madjusmdetlem1  33773  signsw0glem  34530  breprexp  34610  ex-sategoelel  35389  rdgprc0  35757  bj-pr11val  36971  bj-pr22val  36985  mapdhval0  41682  hdmap1val0  41756  refsum2cnlem1  44937  liminf10ex  45695  cncfiooicclem1  45814  fouriersw  46152  hspmbllem1  46547  blen0  48306  0dig1  48343