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

Theorem ifid 4467
Description: Identical true and false arguments in the conditional operator. (Contributed by NM, 18-Apr-2005.)
Assertion
Ref Expression
ifid if(𝜑, 𝐴, 𝐴) = 𝐴

Proof of Theorem ifid
StepHypRef Expression
1 iftrue 4434 . 2 (𝜑 → if(𝜑, 𝐴, 𝐴) = 𝐴)
2 iffalse 4437 . 2 𝜑 → if(𝜑, 𝐴, 𝐴) = 𝐴)
31, 2pm2.61i 185 1 if(𝜑, 𝐴, 𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  ifcif 4428
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 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-if 4429
This theorem is referenced by:  csbif  4483  rabsnif  4622  somincom  5965  fsuppmptif  8851  supsn  8924  infsn  8957  wemaplem2  8999  cantnflem1  9140  xrmaxeq  12564  xrmineq  12565  xaddpnf1  12611  xaddmnf1  12613  rexmul  12656  max0add  14666  sumz  15075  prod1  15294  1arithlem4  16256  xpscf  16834  mgm2nsgrplem2  18080  mgm2nsgrplem3  18081  dmdprdsplitlem  19156  fczpsrbag  20609  mplcoe1  20709  mplcoe3  20710  mplcoe5  20712  evlslem2  20755  mdet0  21215  mdetralt2  21218  mdetunilem9  21229  madurid  21253  decpmatid  21379  cnmpopc  23537  pcoval2  23625  pcorevlem  23635  itgz  24388  itgvallem3  24393  iblposlem  24399  iblss2  24413  itgss  24419  ditg0  24460  cnplimc  24494  limcco  24500  dvexp3  24585  ply1nzb  24727  plyeq0lem  24811  dgrcolem2  24875  plydivlem4  24896  radcnv0  25015  efrlim  25559  mumullem2  25769  lgsval2lem  25895  lgsdilem2  25921  fsuppind  39453  dgrsub2  40076  sqrtcval  40338  relexp1idm  40412  relexp0idm  40413
  Copyright terms: Public domain W3C validator