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

Theorem iftrued 4436
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 4434 . 2 (𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐴)
31, 2syl 17 1 (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = 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:  partfun  6471  mposnif  7251  tz7.44-3  8031  updjudhcoinlf  9349  iunfictbso  9529  ttukeylem7  9930  max0sub  12581  ifle  12582  xmulneg1  12654  xmulpnf1  12659  expnnval  13432  swrdval2  14003  swrdlend  14010  swrd0  14015  relexp0g  14377  max0add  14666  summolem2a  15068  prodmolem2a  15284  ef0lem  15428  rpnnen2lem3  15565  rpnnen2lem9  15571  iserodd  16166  pcmpt  16222  pcmpt2  16223  prmdvdsprmo  16372  fvprif  16830  setcepi  17344  gsumval2a  17891  smndex2dlinvh  18078  mgm2nsgrplem3  18081  mulgnn  18228  pmtrprfv  18577  pmtrprfval  18611  psgnunilem1  18617  dfod2  18687  oddvds2  18689  cyggenod  19000  fincygsubgodd  19231  mplcoe1  20709  mplcoe5  20712  coe1tm  20906  coe1tmmul2fv  20911  coe1pwmulfv  20913  coe1sclmul  20915  coe1sclmul2  20917  m1detdiag  21206  mdetunilem9  21229  maducoeval2  21249  symgmatr01lem  21262  pmatcollpw3fi1lem1  21395  chpmat1dlem  21444  chfacffsupp  21465  chfacfscmul0  21467  chfacfpmmul0  21471  2ndcdisj  22065  dscmet  23183  xrsxmet  23418  cnmpopc  23537  xrhmeo  23555  oprpiece1res1  23560  htpycc  23589  pcoval1  23622  pcohtpylem  23628  pcoass  23633  pcorevlem  23635  ovolunlem1a  24104  ovolunlem1  24105  ovolicc2lem3  24127  ovolicc2lem4  24128  mbfi1fseqlem4  24326  mbfi1fseqlem5  24327  mbfi1fseqlem6  24328  itg2const2  24349  itg2splitlem  24356  itg2split  24357  itg2cnlem1  24369  itg2cnlem2  24370  iblss2  24413  itgspliticc  24444  ditgpos  24463  limcres  24493  plyeq0lem  24811  plypf1  24813  coeeq2  24843  dvply1  24884  aareccl  24926  dvtaylp  24969  pserdvlem2  25027  lgamgulmlem4  25621  isppw  25703  vmappw  25705  muval1  25722  dchrelbasd  25827  dchr1  25845  dchrptlem2  25853  lgsdir2  25918  lgsne0  25923  gausslemma2dlem1a  25953  gausslemma2dlem2  25955  2sqnn0  26026  rplogsumlem2  26073  dchrisum0flblem2  26097  dchrisum0fno1  26099  rplogsum  26115  pntrlog2bndlem5  26169  1loopgrvd2  27297  1hevtxdg1  27300  1egrvtxdg1  27303  crctcshwlkn0lem2  27601  crctcshlem4  27610  crctcsh  27614  clwlkclwwlklem2fv1  27784  eulercrct  28031  eucrct2eupth  28034  pmtridfv1  30791  pmtridfv2  30792  psgnfzto1stlem  30796  ofldchr  30942  smattl  31155  smattr  31156  smatbl  31157  1smat1  31161  madjusmdetlem1  31184  madjusmdetlem2  31185  esumpinfval  31446  eulerpartlemgs2  31752  ballotlemsgt1  31882  ballotlemsel1i  31884  ballotlemsi  31886  signswmnd  31941  signsvtn  31968  cvmliftlem10  32655  unblimceq0lem  33959  poimirlem1  35057  poimirlem2  35058  poimirlem5  35061  poimirlem6  35062  poimirlem12  35068  poimirlem17  35073  poimirlem19  35075  poimirlem20  35076  poimirlem22  35078  poimirlem23  35079  itg2addnc  35110  itg2gt0cn  35111  itgaddnclem2  35115  sdclem1  35180  cdlemefs27cl  37708  metakunt5  39351  metakunt11  39357  metakunt21  39367  metakunt26  39372  metakunt27  39373  metakunt29  39375  metakunt30  39376  flcidc  40111  relexp01min  40407  relexpxpmin  40411  mnurnd  40984  ioondisj2  42123  ioondisj1  42124  lptioo1  42267  limsup10exlem  42407  icccncfext  42522  cncfiooicc  42529  ioodvbdlimc1lem2  42567  ioodvbdlimc2lem  42569  dvnxpaek  42577  ditgeq3d  42599  itgsubsticclem  42610  dirkerper  42731  dirkercncflem2  42739  fourierdlem40  42782  fourierdlem65  42806  fourierdlem74  42815  fourierdlem75  42816  fourierdlem78  42819  fourierdlem81  42822  fourierdlem97  42838  fourierdlem103  42844  fourierdlem104  42845  sqwvfoura  42863  sqwvfourb  42864  fourierswlem  42865  fouriersw  42866  elaa2lem  42868  etransclem19  42888  etransclem22  42891  etransclem24  42893  etransclem35  42904  sge0pnfval  43005  isomenndlem  43162  hoicvrrex  43188  ovn0  43198  volicon0  43207  hsphoidmvle2  43217  hsphoidmvle  43218  hoidmv1lelem1  43223  hoidmv1lelem2  43224  hoidmvlelem2  43228  hoidmvlelem3  43229  hspmbllem1  43258  hspmbllem2  43259  volico2  43273  ovolval2lem  43275  ovnsubadd2lem  43277  ovolval4lem1  43281  vonioolem1  43312  vonioo  43314  vonicclem1  43315  vonicc  43317
  Copyright terms: Public domain W3C validator