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

Theorem iftruei 4432
Description: Inference associated with iftrue 4431. (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 4431 . 2 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
31, 2ax-mp 5 1 if(𝜑, 𝐴, 𝐵) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  ifcif 4425
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-if 4426
This theorem is referenced by:  oe0m  8126  ttukeylem4  9923  xnegpnf  12590  xnegmnf  12591  xaddpnf1  12607  xaddpnf2  12608  xaddmnf1  12609  xaddmnf2  12610  pnfaddmnf  12611  mnfaddpnf  12612  xmul01  12648  exp0  13429  swrd00  13997  sgn0  14440  lcm0val  15928  prmo2  16366  prmo3  16367  prmo5  16454  mulg0  18223  zzngim  20244  obsipid  20411  mvrid  20661  mamulid  21046  mamurid  21047  mat1dimid  21079  scmatf1  21136  mdetdiagid  21205  chpdmatlem3  21445  chpidmat  21452  fclscmpi  22634  ioorinv  24180  ig1pval2  24774  dgrcolem2  24871  plydivlem4  24892  vieta1lem2  24907  0cxp  25257  cxpexp  25259  lgs0  25894  lgs2  25898  2lgs2  25989  axlowdim  26755  1loopgrvd2  27293  eupth2  28024  ex-prmo  28244  madjusmdetlem1  31180  signsw0glem  31933  breprexp  32014  ex-sategoelel  32781  rdgprc0  33151  bj-pr11val  34441  bj-pr22val  34455  mapdhval0  39021  hdmap1val0  39095  refsum2cnlem1  41664  liminf10ex  42414  cncfiooicclem1  42533  fouriersw  42871  hspmbllem1  43263  blen0  44984  0dig1  45021
  Copyright terms: Public domain W3C validator