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

Theorem iftrued 4294
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 4292 . 2 (𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐴)
31, 2syl 17 1 (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  ifcif 4286
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-if 4287
This theorem is referenced by:  mpt2snif  6987  tz7.44-3  7743  updjudhcoinlf  9044  iunfictbso  9223  ttukeylem7  9625  max0sub  12248  ifle  12249  xmulneg1  12320  xmulpnf1  12325  expnnval  13089  swrdval2  13646  swrdlend  13658  swrd0  13661  swrdccatid  13724  relexp0g  13988  max0add  14276  summolem2a  14672  prodmolem2a  14888  ef0lem  15032  rpnnen2lem3  15168  rpnnen2lem9  15174  iserodd  15760  pcmpt  15816  pcmpt2  15817  prmdvdsprmo  15966  setcepi  16945  gsumval2a  17487  mgm2nsgrplem3  17615  mulgnn  17755  pmtrprfv  18077  pmtrprfval  18111  psgnunilem1  18117  dfod2  18185  oddvds2  18187  cyggenod  18490  mplcoe1  19677  mplcoe5  19680  coe1tm  19854  coe1tmmul2fv  19859  coe1pwmulfv  19861  coe1sclmul  19863  coe1sclmul2  19865  m1detdiag  20618  mdetunilem9  20641  maducoeval2  20661  symgmatr01lem  20675  pmatcollpw3fi1lem1  20808  chpmat1dlem  20857  chfacffsupp  20878  chfacfscmul0  20880  chfacfpmmul0  20884  2ndcdisj  21477  dscmet  22594  xrsxmet  22829  cnmpt2pc  22944  xrhmeo  22962  oprpiece1res1  22967  htpycc  22996  pcoval1  23029  pcohtpylem  23035  pcoass  23040  pcorevlem  23042  ovolunlem1a  23483  ovolunlem1  23484  ovolicc2lem3  23506  ovolicc2lem4  23507  mbfi1fseqlem4  23705  mbfi1fseqlem5  23706  mbfi1fseqlem6  23707  itg2const2  23728  itg2splitlem  23735  itg2split  23736  itg2cnlem1  23748  itg2cnlem2  23749  iblss2  23792  itgspliticc  23823  ditgpos  23840  limcres  23870  plyeq0lem  24186  plypf1  24188  coeeq2  24218  dvply1  24259  aareccl  24301  dvtaylp  24344  pserdvlem2  24402  lgamgulmlem4  24978  isppw  25060  vmappw  25062  muval1  25079  dchrelbasd  25184  dchr1  25202  dchrptlem2  25210  lgsdir2  25275  lgsne0  25280  gausslemma2dlem1a  25310  gausslemma2dlem2  25312  rplogsumlem2  25394  dchrisum0flblem2  25418  dchrisum0fno1  25420  rplogsum  25436  pntrlog2bndlem5  25490  1loopgrvd2  26633  1hevtxdg1  26636  1egrvtxdg1  26639  crctcshwlkn0lem2  26938  crctcshlem4  26947  crctcsh  26951  clwlkclwwlklem2fv1  27144  eulercrct  27421  eucrct2eupth  27424  partfun  29808  ofldchr  30145  psgnfzto1stlem  30181  pmtridfv1  30188  pmtridfv2  30189  smattl  30195  smattr  30196  smatbl  30197  1smat1  30201  madjusmdetlem1  30224  madjusmdetlem2  30225  esumpinfval  30466  eulerpartlemgs2  30773  ballotlemsgt1  30903  ballotlemsel1i  30905  ballotlemsi  30907  signswmnd  30965  signsvtn  30992  cvmliftlem10  31604  unblimceq0lem  32819  poimirlem1  33725  poimirlem2  33726  poimirlem5  33729  poimirlem6  33730  poimirlem12  33736  poimirlem17  33741  poimirlem19  33743  poimirlem20  33744  poimirlem22  33746  poimirlem23  33747  itg2addnc  33778  itg2gt0cn  33779  itgaddnclem2  33783  sdclem1  33852  cdlemefs27cl  36195  flcidc  38246  relexp01min  38506  relexpxpmin  38510  ioondisj2  40199  ioondisj1  40200  lptioo1  40345  limsup10exlem  40485  icccncfext  40581  cncfiooicc  40588  ioodvbdlimc1lem2  40628  ioodvbdlimc2lem  40630  dvnxpaek  40638  ditgeq3d  40660  itgsubsticclem  40671  dirkerper  40793  dirkercncflem2  40801  fourierdlem40  40844  fourierdlem65  40868  fourierdlem74  40877  fourierdlem75  40878  fourierdlem78  40881  fourierdlem81  40884  fourierdlem97  40900  fourierdlem103  40906  fourierdlem104  40907  sqwvfoura  40925  sqwvfourb  40926  fourierswlem  40927  fouriersw  40928  elaa2lem  40930  etransclem19  40950  etransclem22  40953  etransclem24  40955  etransclem35  40966  sge0pnfval  41070  isomenndlem  41227  hoicvrrex  41253  ovn0  41263  volicon0  41272  hsphoidmvle2  41282  hsphoidmvle  41283  hoidmv1lelem1  41288  hoidmv1lelem2  41289  hoidmvlelem2  41293  hoidmvlelem3  41294  hspmbllem1  41323  hspmbllem2  41324  volico2  41338  ovolval2lem  41340  ovnsubadd2lem  41342  ovolval4lem1  41346  vonioolem1  41377  vonioo  41379  vonicclem1  41380  vonicc  41382
  Copyright terms: Public domain W3C validator