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

Theorem iftruei 4070
Description: Inference associated with iftrue 4069. (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 4069 . 2 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
31, 2ax-mp 5 1 if(𝜑, 𝐴, 𝐵) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  ifcif 4063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-if 4064
This theorem is referenced by:  oe0m  7550  ttukeylem4  9286  xnegpnf  11991  xnegmnf  11992  xaddpnf1  12008  xaddpnf2  12009  xaddmnf1  12010  xaddmnf2  12011  pnfaddmnf  12012  mnfaddpnf  12013  xmul01  12048  exp0  12812  swrd00  13364  sgn0  13771  lcm0val  15242  prmo2  15679  prmo3  15680  prmo5  15771  mulg0  17478  mvrid  19355  zzngim  19833  obsipid  19998  mamulid  20179  mamurid  20180  mat1dimid  20212  scmatf1  20269  mdetdiagid  20338  chpdmatlem3  20577  chpidmat  20584  fclscmpi  21756  ioorinv  23267  ig1pval2  23854  dgrcolem2  23951  plydivlem4  23972  vieta1lem2  23987  0cxp  24329  cxpexp  24331  lgs0  24952  lgs2  24956  2lgs2  25047  axlowdim  25758  1loopgrvd2  26302  eupth2  26982  ex-prmo  27187  madjusmdetlem1  29699  signsw0glem  30434  rdgprc0  31435  bj-pr11val  32675  bj-pr22val  32689  mapdhval0  36529  hdmap1val0  36604  refsum2cnlem1  38714  cncfiooicclem1  39437  fouriersw  39781  hspmbllem1  40173  blen0  41684  0dig1  41721
  Copyright terms: Public domain W3C validator