Theorem iftrued 4475

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

Step	Hyp	Ref	Expression
1		iftrued.1	. 2 ⊢ (𝜑 → 𝜒)
2		iftrue 4473	. 2 ⊢ (𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1542  ifcif 4467

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4468

This theorem is referenced by:  partfun  6639  mposnif  7476  tz7.44-3  8340  ttrcltr  9628  updjudhcoinlf  9847  iunfictbso  10027  ttukeylem7  10428  max0sub  13139  ifle  13140  xmulneg1  13212  xmulpnf1  13217  expnnval  14017  swrdval2  14600  swrdlend  14607  swrd0  14612  relexp0g  14975  max0add  15263  summolem2a  15668  prodmolem2a  15890  ef0lem  16034  rpnnen2lem3  16174  rpnnen2lem9  16180  iserodd  16797  pcmpt  16854  pcmpt2  16855  prmdvdsprmo  17004  fvprif  17516  setcepi  18046  gsumval2a  18644  smndex2dlinvh  18879  mgm2nsgrplem3  18882  mulgnn  19042  pmtrprfv  19419  pmtrprfval  19453  psgnunilem1  19459  dfod2  19530  oddvds2  19532  cyggenod  19850  fincygsubgodd  20080  ofldchr  21566  mplcoe1  22025  mplcoe5  22028  coe1tm  22248  coe1tmmul2fv  22253  coe1pwmulfv  22255  coe1sclmul  22257  coe1sclmul2  22259  m1detdiag  22572  mdetunilem9  22595  maducoeval2  22615  symgmatr01lem  22628  pmatcollpw3fi1lem1  22761  chpmat1dlem  22810  chfacffsupp  22831  chfacfscmul0  22833  chfacfpmmul0  22837  2ndcdisj  23431  dscmet  24547  xrsxmet  24785  cnmpopc  24905  xrhmeo  24923  oprpiece1res1  24928  htpycc  24957  pcoval1  24990  pcohtpylem  24996  pcoass  25001  pcorevlem  25003  ovolunlem1a  25473  ovolunlem1  25474  ovolicc2lem3  25496  ovolicc2lem4  25497  mbfi1fseqlem4  25695  mbfi1fseqlem5  25696  mbfi1fseqlem6  25697  itg2const2  25718  itg2splitlem  25725  itg2split  25726  itg2cnlem1  25738  itg2cnlem2  25739  iblss2  25783  itgspliticc  25814  ditgpos  25833  limcres  25863  plyeq0lem  26185  plypf1  26187  coeeq2  26217  dvply1  26260  aareccl  26303  dvtaylp  26347  pserdvlem2  26406  lgamgulmlem4  27009  isppw  27091  vmappw  27093  muval1  27110  dchrelbasd  27216  dchr1  27234  dchrptlem2  27242  lgsdir2  27307  lgsne0  27312  gausslemma2dlem1a  27342  gausslemma2dlem2  27344  2sqnn0  27415  rplogsumlem2  27462  dchrisum0flblem2  27486  dchrisum0fno1  27488  rplogsum  27504  pntrlog2bndlem5  27558  noinfbnd2  27709  expnnsval  28432  1loopgrvd2  29587  1hevtxdg1  29590  1egrvtxdg1  29593  crctcshwlkn0lem2  29894  crctcshlem4  29903  crctcsh  29907  clwlkclwwlklem2fv1  30080  eulercrct  30327  eucrct2eupth  30330  ccatws1f1o  33026  pmtridfv1  33171  pmtridfv2  33172  psgnfzto1stlem  33176  elrgspnlem2  33319  elrgspnlem3  33320  elrspunsn  33504  gsummoncoe1fzo  33672  evlextv  33701  esplyind  33734  vieta  33739  fldextrspunlsp  33834  extdgfialglem2  33853  rtelextdg2lem  33886  2sqr3minply  33940  smattl  33958  smattr  33959  smatbl  33960  1smat1  33964  madjusmdetlem1  33987  madjusmdetlem2  33988  esumpinfval  34233  eulerpartlemgs2  34540  ballotlemsgt1  34671  ballotlemsel1i  34673  ballotlemsi  34675  signswmnd  34717  signsvtn  34744  cvmliftlem10  35492  unblimceq0lem  36782  bj-rdg0gALT  37394  poimirlem1  37956  poimirlem2  37957  poimirlem5  37960  poimirlem6  37961  poimirlem12  37967  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem22  37977  poimirlem23  37978  itg2addnc  38009  itg2gt0cn  38010  itgaddnclem2  38014  sdclem1  38078  cdlemefs27cl  40873  sticksstones9  42607  sticksstones10  42608  sticksstones12a  42610  unitscyglem1  42648  flcidc  43616  oe0suclim  43723  tfsconcatfv  43787  safesnsupfilb  43863  relexp01min  44158  relexpxpmin  44162  mnurnd  44728  ioondisj2  45941  ioondisj1  45942  lptioo1  46080  limsup10exlem  46218  icccncfext  46333  cncfiooicc  46340  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvnxpaek  46388  ditgeq3d  46410  itgsubsticclem  46421  dirkerper  46542  dirkercncflem2  46550  fourierdlem40  46593  fourierdlem65  46617  fourierdlem74  46626  fourierdlem75  46627  fourierdlem78  46630  fourierdlem81  46633  fourierdlem97  46649  fourierdlem103  46655  fourierdlem104  46656  sqwvfoura  46674  sqwvfourb  46675  fourierswlem  46676  fouriersw  46677  elaa2lem  46679  etransclem19  46699  etransclem22  46702  etransclem24  46704  etransclem35  46715  sge0pnfval  46819  isomenndlem  46976  hoicvrrex  47002  ovn0  47012  volicon0  47021  hsphoidmvle2  47031  hsphoidmvle  47032  hoidmv1lelem1  47037  hoidmv1lelem2  47038  hoidmvlelem2  47042  hoidmvlelem3  47043  hspmbllem1  47072  hspmbllem2  47073  volico2  47087  ovolval2lem  47089  ovnsubadd2lem  47091  ovolval4lem1  47095  vonioolem1  47126  vonioo  47128  vonicclem1  47129  vonicc  47131  discsubc  49551  oppf1st2nd  49618  2oppf  49619  oppfval  49623