MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iftruei Structured version   Visualization version   GIF version

Theorem iftruei 4233
Description: Inference associated with iftrue 4232. (Contributed by BJ, 7-Oct-2018.)
Hypothesis
Ref Expression
iftruei.1 𝜑
Assertion
Ref Expression
iftruei if(𝜑, 𝐴, 𝐵) = 𝐴

Proof of Theorem iftruei
StepHypRef Expression
1 iftruei.1 . 2 𝜑
2 iftrue 4232 . 2 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
31, 2ax-mp 5 1 if(𝜑, 𝐴, 𝐵) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  ifcif 4226
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-if 4227
This theorem is referenced by:  oe0m  7755  ttukeylem4  9539  xnegpnf  12244  xnegmnf  12245  xaddpnf1  12261  xaddpnf2  12262  xaddmnf1  12263  xaddmnf2  12264  pnfaddmnf  12265  mnfaddpnf  12266  xmul01  12301  exp0  13070  swrd00  13625  sgn0  14036  lcm0val  15514  prmo2  15950  prmo3  15951  prmo5  16042  mulg0  17753  mvrid  19637  zzngim  20115  obsipid  20282  mamulid  20463  mamurid  20464  mat1dimid  20497  scmatf1  20554  mdetdiagid  20623  chpdmatlem3  20864  chpidmat  20871  fclscmpi  22052  ioorinv  23563  ig1pval2  24152  dgrcolem2  24249  plydivlem4  24270  vieta1lem2  24285  0cxp  24632  cxpexp  24634  lgs0  25255  lgs2  25259  2lgs2  25350  axlowdim  26061  1loopgrvd2  26633  eupth2  27418  ex-prmo  27657  madjusmdetlem1  30232  signsw0glem  30969  breprexp  31050  rdgprc0  32034  bj-pr11val  33323  bj-pr22val  33337  mapdhval0  37535  hdmap1val0  37609  refsum2cnlem1  39718  liminf10ex  40521  cncfiooicclem1  40621  fouriersw  40962  hspmbllem1  41357  blen0  42891  0dig1  42928
  Copyright terms: Public domain W3C validator