Theorem iftruei 4538

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

Syntax hints:   = wceq 1537  ifcif 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-if 4532

This theorem is referenced by:  oe0m  8555  ttrcltr  9754  ttukeylem4  10550  xnegpnf  13248  xnegmnf  13249  xaddpnf1  13265  xaddpnf2  13266  xaddmnf1  13267  xaddmnf2  13268  pnfaddmnf  13269  mnfaddpnf  13270  xmul01  13306  exp0  14103  swrd00  14679  sgn0  15125  lcm0val  16628  prmo2  17074  prmo3  17075  prmo5  17163  mulg0  19105  zzngim  21589  obsipid  21760  mvrid  22022  mamulid  22463  mamurid  22464  mat1dimid  22496  scmatf1  22553  mdetdiagid  22622  chpdmatlem3  22862  chpidmat  22869  fclscmpi  24053  ioorinv  25625  ig1pval2  26231  dgrcolem2  26329  plydivlem4  26353  vieta1lem2  26368  0cxp  26723  cxpexp  26725  lgs0  27369  lgs2  27373  2lgs2  27464  left1s  27948  exps0  28425  axlowdim  28991  1loopgrvd2  29536  eupth2  30268  ex-prmo  30488  madjusmdetlem1  33788  signsw0glem  34547  breprexp  34627  ex-sategoelel  35406  rdgprc0  35775  bj-pr11val  36988  bj-pr22val  37002  mapdhval0  41708  hdmap1val0  41782  refsum2cnlem1  44975  liminf10ex  45730  cncfiooicclem1  45849  fouriersw  46187  hspmbllem1  46582  blen0  48422  0dig1  48459