Theorem iftruei 4093

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

Syntax hints:   = wceq 1483  ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  oe0m  7598  ttukeylem4  9334  xnegpnf  12040  xnegmnf  12041  xaddpnf1  12057  xaddpnf2  12058  xaddmnf1  12059  xaddmnf2  12060  pnfaddmnf  12061  mnfaddpnf  12062  xmul01  12097  exp0  12864  swrd00  13418  sgn0  13829  lcm0val  15307  prmo2  15744  prmo3  15745  prmo5  15836  mulg0  17546  mvrid  19423  zzngim  19901  obsipid  20066  mamulid  20247  mamurid  20248  mat1dimid  20280  scmatf1  20337  mdetdiagid  20406  chpdmatlem3  20645  chpidmat  20652  fclscmpi  21833  ioorinv  23344  ig1pval2  23933  dgrcolem2  24030  plydivlem4  24051  vieta1lem2  24066  0cxp  24412  cxpexp  24414  lgs0  25035  lgs2  25039  2lgs2  25130  axlowdim  25841  1loopgrvd2  26399  eupth2  27099  ex-prmo  27316  madjusmdetlem1  29893  signsw0glem  30630  breprexp  30711  rdgprc0  31699  bj-pr11val  32993  bj-pr22val  33007  mapdhval0  37014  hdmap1val0  37089  refsum2cnlem1  39196  liminf10ex  40006  cncfiooicclem1  40106  fouriersw  40448  hspmbllem1  40840  blen0  42366  0dig1  42403