Theorem iftruei 4536

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

Syntax hints:   = wceq 1542  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4530

This theorem is referenced by:  oe0m  8518  ttrcltr  9711  ttukeylem4  10507  xnegpnf  13188  xnegmnf  13189  xaddpnf1  13205  xaddpnf2  13206  xaddmnf1  13207  xaddmnf2  13208  pnfaddmnf  13209  mnfaddpnf  13210  xmul01  13246  exp0  14031  swrd00  14594  sgn0  15036  lcm0val  16531  prmo2  16973  prmo3  16974  prmo5  17062  mulg0  18957  zzngim  21108  obsipid  21277  mvrid  21543  mamulid  21943  mamurid  21944  mat1dimid  21976  scmatf1  22033  mdetdiagid  22102  chpdmatlem3  22342  chpidmat  22349  fclscmpi  23533  ioorinv  25093  ig1pval2  25691  dgrcolem2  25788  plydivlem4  25809  vieta1lem2  25824  0cxp  26174  cxpexp  26176  lgs0  26813  lgs2  26817  2lgs2  26908  left1s  27389  axlowdim  28219  1loopgrvd2  28760  eupth2  29492  ex-prmo  29712  madjusmdetlem1  32807  signsw0glem  33564  breprexp  33645  ex-sategoelel  34412  rdgprc0  34765  bj-pr11val  35886  bj-pr22val  35900  mapdhval0  40596  hdmap1val0  40670  refsum2cnlem1  43721  liminf10ex  44490  cncfiooicclem1  44609  fouriersw  44947  hspmbllem1  45342  blen0  47258  0dig1  47295