Theorem iftrued 4482

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 4480	. 2 ⊢ (𝜒 → if(𝜒, 𝐴, 𝐵) = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1541  ifcif 4474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-if 4475

This theorem is referenced by:  partfun  6633  mposnif  7468  tz7.44-3  8333  ttrcltr  9613  updjudhcoinlf  9832  iunfictbso  10012  ttukeylem7  10413  max0sub  13097  ifle  13098  xmulneg1  13170  xmulpnf1  13175  expnnval  13973  swrdval2  14556  swrdlend  14563  swrd0  14568  relexp0g  14931  max0add  15219  summolem2a  15624  prodmolem2a  15843  ef0lem  15987  rpnnen2lem3  16127  rpnnen2lem9  16133  iserodd  16749  pcmpt  16806  pcmpt2  16807  prmdvdsprmo  16956  fvprif  17467  setcepi  17997  gsumval2a  18595  smndex2dlinvh  18827  mgm2nsgrplem3  18830  mulgnn  18990  pmtrprfv  19367  pmtrprfval  19401  psgnunilem1  19407  dfod2  19478  oddvds2  19480  cyggenod  19798  fincygsubgodd  20028  ofldchr  21515  mplcoe1  21973  mplcoe5  21976  coe1tm  22188  coe1tmmul2fv  22193  coe1pwmulfv  22195  coe1sclmul  22197  coe1sclmul2  22199  m1detdiag  22513  mdetunilem9  22536  maducoeval2  22556  symgmatr01lem  22569  pmatcollpw3fi1lem1  22702  chpmat1dlem  22751  chfacffsupp  22772  chfacfscmul0  22774  chfacfpmmul0  22778  2ndcdisj  23372  dscmet  24488  xrsxmet  24726  cnmpopc  24850  xrhmeo  24872  oprpiece1res1  24877  htpycc  24907  pcoval1  24941  pcohtpylem  24947  pcoass  24952  pcorevlem  24954  ovolunlem1a  25425  ovolunlem1  25426  ovolicc2lem3  25448  ovolicc2lem4  25449  mbfi1fseqlem4  25647  mbfi1fseqlem5  25648  mbfi1fseqlem6  25649  itg2const2  25670  itg2splitlem  25677  itg2split  25678  itg2cnlem1  25690  itg2cnlem2  25691  iblss2  25735  itgspliticc  25766  ditgpos  25785  limcres  25815  plyeq0lem  26143  plypf1  26145  coeeq2  26175  dvply1  26219  aareccl  26262  dvtaylp  26306  pserdvlem2  26366  lgamgulmlem4  26970  isppw  27052  vmappw  27054  muval1  27071  dchrelbasd  27178  dchr1  27196  dchrptlem2  27204  lgsdir2  27269  lgsne0  27274  gausslemma2dlem1a  27304  gausslemma2dlem2  27306  2sqnn0  27377  rplogsumlem2  27424  dchrisum0flblem2  27448  dchrisum0fno1  27450  rplogsum  27466  pntrlog2bndlem5  27520  noinfbnd2  27671  expsnnval  28350  1loopgrvd2  29484  1hevtxdg1  29487  1egrvtxdg1  29490  crctcshwlkn0lem2  29791  crctcshlem4  29800  crctcsh  29804  clwlkclwwlklem2fv1  29977  eulercrct  30224  eucrct2eupth  30227  ccatws1f1o  32939  pmtridfv1  33071  pmtridfv2  33072  psgnfzto1stlem  33076  elrgspnlem2  33217  elrgspnlem3  33218  elrspunsn  33401  gsummoncoe1fzo  33565  esplyind  33613  fldextrspunlsp  33708  extdgfialglem2  33727  rtelextdg2lem  33760  2sqr3minply  33814  smattl  33832  smattr  33833  smatbl  33834  1smat1  33838  madjusmdetlem1  33861  madjusmdetlem2  33862  esumpinfval  34107  eulerpartlemgs2  34414  ballotlemsgt1  34545  ballotlemsel1i  34547  ballotlemsi  34549  signswmnd  34591  signsvtn  34618  cvmliftlem10  35359  unblimceq0lem  36571  bj-rdg0gALT  37136  poimirlem1  37681  poimirlem2  37682  poimirlem5  37685  poimirlem6  37686  poimirlem12  37692  poimirlem17  37697  poimirlem19  37699  poimirlem20  37700  poimirlem22  37702  poimirlem23  37703  itg2addnc  37734  itg2gt0cn  37735  itgaddnclem2  37739  sdclem1  37803  cdlemefs27cl  40532  sticksstones9  42267  sticksstones10  42268  sticksstones12a  42270  unitscyglem1  42308  flcidc  43287  oe0suclim  43394  tfsconcatfv  43458  safesnsupfilb  43535  relexp01min  43830  relexpxpmin  43834  mnurnd  44400  ioondisj2  45617  ioondisj1  45618  lptioo1  45756  limsup10exlem  45894  icccncfext  46009  cncfiooicc  46016  ioodvbdlimc1lem2  46054  ioodvbdlimc2lem  46056  dvnxpaek  46064  ditgeq3d  46086  itgsubsticclem  46097  dirkerper  46218  dirkercncflem2  46226  fourierdlem40  46269  fourierdlem65  46293  fourierdlem74  46302  fourierdlem75  46303  fourierdlem78  46306  fourierdlem81  46309  fourierdlem97  46325  fourierdlem103  46331  fourierdlem104  46332  sqwvfoura  46350  sqwvfourb  46351  fourierswlem  46352  fouriersw  46353  elaa2lem  46355  etransclem19  46375  etransclem22  46378  etransclem24  46380  etransclem35  46391  sge0pnfval  46495  isomenndlem  46652  hoicvrrex  46678  ovn0  46688  volicon0  46697  hsphoidmvle2  46707  hsphoidmvle  46708  hoidmv1lelem1  46713  hoidmv1lelem2  46714  hoidmvlelem2  46718  hoidmvlelem3  46719  hspmbllem1  46748  hspmbllem2  46749  volico2  46763  ovolval2lem  46765  ovnsubadd2lem  46767  ovolval4lem1  46771  vonioolem1  46802  vonioo  46804  vonicclem1  46805  vonicc  46807  discsubc  49189  oppf1st2nd  49256  2oppf  49257  oppfval  49261