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

Theorem iftrued 4471
Description: Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
iftrued.1 (𝜑𝜒)
Assertion
Ref Expression
iftrued (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)

Proof of Theorem iftrued
StepHypRef Expression
1 iftrued.1 . 2 (𝜑𝜒)
2 iftrue 4469 . 2 (𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐴)
31, 2syl 17 1 (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  ifcif 4463
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-if 4464
This theorem is referenced by:  mposnif  7257  tz7.44-3  8033  updjudhcoinlf  9349  iunfictbso  9528  ttukeylem7  9925  max0sub  12577  ifle  12578  xmulneg1  12650  xmulpnf1  12655  expnnval  13420  swrdval2  13996  swrdlend  14003  swrd0  14008  relexp0g  14369  max0add  14658  summolem2a  15060  prodmolem2a  15276  ef0lem  15420  rpnnen2lem3  15557  rpnnen2lem9  15563  iserodd  16160  pcmpt  16216  pcmpt2  16217  prmdvdsprmo  16366  fvprif  16822  setcepi  17336  gsumval2a  17883  mgm2nsgrplem3  18023  mulgnn  18170  pmtrprfv  18510  pmtrprfval  18544  psgnunilem1  18550  dfod2  18620  oddvds2  18622  cyggenod  18932  fincygsubgodd  19163  mplcoe1  20174  mplcoe5  20177  coe1tm  20369  coe1tmmul2fv  20374  coe1pwmulfv  20376  coe1sclmul  20378  coe1sclmul2  20380  m1detdiag  21134  mdetunilem9  21157  maducoeval2  21177  symgmatr01lem  21190  pmatcollpw3fi1lem1  21322  chpmat1dlem  21371  chfacffsupp  21392  chfacfscmul0  21394  chfacfpmmul0  21398  2ndcdisj  21992  dscmet  23109  xrsxmet  23344  cnmpopc  23459  xrhmeo  23477  oprpiece1res1  23482  htpycc  23511  pcoval1  23544  pcohtpylem  23550  pcoass  23555  pcorevlem  23557  ovolunlem1a  24024  ovolunlem1  24025  ovolicc2lem3  24047  ovolicc2lem4  24048  mbfi1fseqlem4  24246  mbfi1fseqlem5  24247  mbfi1fseqlem6  24248  itg2const2  24269  itg2splitlem  24276  itg2split  24277  itg2cnlem1  24289  itg2cnlem2  24290  iblss2  24333  itgspliticc  24364  ditgpos  24381  limcres  24411  plyeq0lem  24727  plypf1  24729  coeeq2  24759  dvply1  24800  aareccl  24842  dvtaylp  24885  pserdvlem2  24943  lgamgulmlem4  25536  isppw  25618  vmappw  25620  muval1  25637  dchrelbasd  25742  dchr1  25760  dchrptlem2  25768  lgsdir2  25833  lgsne0  25838  gausslemma2dlem1a  25868  gausslemma2dlem2  25870  2sqnn0  25941  rplogsumlem2  25988  dchrisum0flblem2  26012  dchrisum0fno1  26014  rplogsum  26030  pntrlog2bndlem5  26084  1loopgrvd2  27212  1hevtxdg1  27215  1egrvtxdg1  27218  crctcshwlkn0lem2  27516  crctcshlem4  27525  crctcsh  27529  clwlkclwwlklem2fv1  27700  eulercrct  27948  eucrct2eupth  27951  partfun  30349  pmtridfv1  30664  pmtridfv2  30665  psgnfzto1stlem  30669  ofldchr  30814  smattl  30962  smattr  30963  smatbl  30964  1smat1  30968  madjusmdetlem1  30991  madjusmdetlem2  30992  esumpinfval  31231  eulerpartlemgs2  31537  ballotlemsgt1  31667  ballotlemsel1i  31669  ballotlemsi  31671  signswmnd  31726  signsvtn  31753  cvmliftlem10  32438  unblimceq0lem  33742  poimirlem1  34774  poimirlem2  34775  poimirlem5  34778  poimirlem6  34779  poimirlem12  34785  poimirlem17  34790  poimirlem19  34792  poimirlem20  34793  poimirlem22  34795  poimirlem23  34796  itg2addnc  34827  itg2gt0cn  34828  itgaddnclem2  34832  sdclem1  34899  cdlemefs27cl  37429  flcidc  39652  relexp01min  39936  relexpxpmin  39940  mnurnd  40496  ioondisj2  41643  ioondisj1  41644  lptioo1  41789  limsup10exlem  41929  icccncfext  42046  cncfiooicc  42053  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  dvnxpaek  42103  ditgeq3d  42125  itgsubsticclem  42136  dirkerper  42258  dirkercncflem2  42266  fourierdlem40  42309  fourierdlem65  42333  fourierdlem74  42342  fourierdlem75  42343  fourierdlem78  42346  fourierdlem81  42349  fourierdlem97  42365  fourierdlem103  42371  fourierdlem104  42372  sqwvfoura  42390  sqwvfourb  42391  fourierswlem  42392  fouriersw  42393  elaa2lem  42395  etransclem19  42415  etransclem22  42418  etransclem24  42420  etransclem35  42431  sge0pnfval  42532  isomenndlem  42689  hoicvrrex  42715  ovn0  42725  volicon0  42734  hsphoidmvle2  42744  hsphoidmvle  42745  hoidmv1lelem1  42750  hoidmv1lelem2  42751  hoidmvlelem2  42755  hoidmvlelem3  42756  hspmbllem1  42785  hspmbllem2  42786  volico2  42800  ovolval2lem  42802  ovnsubadd2lem  42804  ovolval4lem1  42808  vonioolem1  42839  vonioo  42841  vonicclem1  42842  vonicc  42844  smndex2dlinvh  44017
  Copyright terms: Public domain W3C validator