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

Theorem iftrued 4495
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 4493 . 2 (𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐴)
31, 2syl 17 1 (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  ifcif 4487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-if 4488
This theorem is referenced by:  partfun  6649  mposnif  7473  tz7.44-3  8355  ttrcltr  9653  updjudhcoinlf  9869  iunfictbso  10051  ttukeylem7  10452  max0sub  13116  ifle  13117  xmulneg1  13189  xmulpnf1  13194  expnnval  13971  swrdval2  14535  swrdlend  14542  swrd0  14547  relexp0g  14908  max0add  15196  summolem2a  15601  prodmolem2a  15818  ef0lem  15962  rpnnen2lem3  16099  rpnnen2lem9  16105  iserodd  16708  pcmpt  16765  pcmpt2  16766  prmdvdsprmo  16915  fvprif  17444  setcepi  17975  gsumval2a  18541  smndex2dlinvh  18728  mgm2nsgrplem3  18731  mulgnn  18881  pmtrprfv  19236  pmtrprfval  19270  psgnunilem1  19276  dfod2  19347  oddvds2  19349  cyggenod  19662  fincygsubgodd  19892  mplcoe1  21441  mplcoe5  21444  coe1tm  21647  coe1tmmul2fv  21652  coe1pwmulfv  21654  coe1sclmul  21656  coe1sclmul2  21658  m1detdiag  21949  mdetunilem9  21972  maducoeval2  21992  symgmatr01lem  22005  pmatcollpw3fi1lem1  22138  chpmat1dlem  22187  chfacffsupp  22208  chfacfscmul0  22210  chfacfpmmul0  22214  2ndcdisj  22810  dscmet  23931  xrsxmet  24175  cnmpopc  24294  xrhmeo  24312  oprpiece1res1  24317  htpycc  24346  pcoval1  24379  pcohtpylem  24385  pcoass  24390  pcorevlem  24392  ovolunlem1a  24863  ovolunlem1  24864  ovolicc2lem3  24886  ovolicc2lem4  24887  mbfi1fseqlem4  25086  mbfi1fseqlem5  25087  mbfi1fseqlem6  25088  itg2const2  25109  itg2splitlem  25116  itg2split  25117  itg2cnlem1  25129  itg2cnlem2  25130  iblss2  25173  itgspliticc  25204  ditgpos  25223  limcres  25253  plyeq0lem  25574  plypf1  25576  coeeq2  25606  dvply1  25647  aareccl  25689  dvtaylp  25732  pserdvlem2  25790  lgamgulmlem4  26384  isppw  26466  vmappw  26468  muval1  26485  dchrelbasd  26590  dchr1  26608  dchrptlem2  26616  lgsdir2  26681  lgsne0  26686  gausslemma2dlem1a  26716  gausslemma2dlem2  26718  2sqnn0  26789  rplogsumlem2  26836  dchrisum0flblem2  26860  dchrisum0fno1  26862  rplogsum  26878  pntrlog2bndlem5  26932  noinfbnd2  27082  1loopgrvd2  28454  1hevtxdg1  28457  1egrvtxdg1  28460  crctcshwlkn0lem2  28759  crctcshlem4  28768  crctcsh  28772  clwlkclwwlklem2fv1  28942  eulercrct  29189  eucrct2eupth  29192  pmtridfv1  31947  pmtridfv2  31948  psgnfzto1stlem  31952  ofldchr  32112  smattl  32382  smattr  32383  smatbl  32384  1smat1  32388  madjusmdetlem1  32411  madjusmdetlem2  32412  esumpinfval  32675  eulerpartlemgs2  32983  ballotlemsgt1  33113  ballotlemsel1i  33115  ballotlemsi  33117  signswmnd  33172  signsvtn  33199  cvmliftlem10  33891  unblimceq0lem  34972  bj-rdg0gALT  35545  poimirlem1  36082  poimirlem2  36083  poimirlem5  36086  poimirlem6  36087  poimirlem12  36093  poimirlem17  36098  poimirlem19  36100  poimirlem20  36101  poimirlem22  36103  poimirlem23  36104  itg2addnc  36135  itg2gt0cn  36136  itgaddnclem2  36140  sdclem1  36205  cdlemefs27cl  38879  sticksstones9  40565  sticksstones10  40566  sticksstones12a  40568  metakunt5  40584  metakunt11  40590  metakunt21  40600  metakunt26  40605  metakunt27  40606  metakunt29  40608  metakunt30  40609  metakunt31  40610  flcidc  41504  oe0suclim  41615  safesnsupfilb  41697  relexp01min  41992  relexpxpmin  41996  mnurnd  42570  ioondisj2  43738  ioondisj1  43739  lptioo1  43880  limsup10exlem  44020  icccncfext  44135  cncfiooicc  44142  ioodvbdlimc1lem2  44180  ioodvbdlimc2lem  44182  dvnxpaek  44190  ditgeq3d  44212  itgsubsticclem  44223  dirkerper  44344  dirkercncflem2  44352  fourierdlem40  44395  fourierdlem65  44419  fourierdlem74  44428  fourierdlem75  44429  fourierdlem78  44432  fourierdlem81  44435  fourierdlem97  44451  fourierdlem103  44457  fourierdlem104  44458  sqwvfoura  44476  sqwvfourb  44477  fourierswlem  44478  fouriersw  44479  elaa2lem  44481  etransclem19  44501  etransclem22  44504  etransclem24  44506  etransclem35  44517  sge0pnfval  44621  isomenndlem  44778  hoicvrrex  44804  ovn0  44814  volicon0  44823  hsphoidmvle2  44833  hsphoidmvle  44834  hoidmv1lelem1  44839  hoidmv1lelem2  44840  hoidmvlelem2  44844  hoidmvlelem3  44845  hspmbllem1  44874  hspmbllem2  44875  volico2  44889  ovolval2lem  44891  ovnsubadd2lem  44893  ovolval4lem1  44897  vonioolem1  44928  vonioo  44930  vonicclem1  44931  vonicc  44933
  Copyright terms: Public domain W3C validator