Theorem iftrued 4489

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

Syntax hints:   → wi 4   = wceq 1542  ifcif 4481

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 4482

This theorem is referenced by:  partfun  6647  mposnif  7484  tz7.44-3  8349  ttrcltr  9637  updjudhcoinlf  9856  iunfictbso  10036  ttukeylem7  10437  max0sub  13123  ifle  13124  xmulneg1  13196  xmulpnf1  13201  expnnval  13999  swrdval2  14582  swrdlend  14589  swrd0  14594  relexp0g  14957  max0add  15245  summolem2a  15650  prodmolem2a  15869  ef0lem  16013  rpnnen2lem3  16153  rpnnen2lem9  16159  iserodd  16775  pcmpt  16832  pcmpt2  16833  prmdvdsprmo  16982  fvprif  17494  setcepi  18024  gsumval2a  18622  smndex2dlinvh  18854  mgm2nsgrplem3  18857  mulgnn  19017  pmtrprfv  19394  pmtrprfval  19428  psgnunilem1  19434  dfod2  19505  oddvds2  19507  cyggenod  19825  fincygsubgodd  20055  ofldchr  21543  mplcoe1  22004  mplcoe5  22007  coe1tm  22227  coe1tmmul2fv  22232  coe1pwmulfv  22234  coe1sclmul  22236  coe1sclmul2  22238  m1detdiag  22553  mdetunilem9  22576  maducoeval2  22596  symgmatr01lem  22609  pmatcollpw3fi1lem1  22742  chpmat1dlem  22791  chfacffsupp  22812  chfacfscmul0  22814  chfacfpmmul0  22818  2ndcdisj  23412  dscmet  24528  xrsxmet  24766  cnmpopc  24890  xrhmeo  24912  oprpiece1res1  24917  htpycc  24947  pcoval1  24981  pcohtpylem  24987  pcoass  24992  pcorevlem  24994  ovolunlem1a  25465  ovolunlem1  25466  ovolicc2lem3  25488  ovolicc2lem4  25489  mbfi1fseqlem4  25687  mbfi1fseqlem5  25688  mbfi1fseqlem6  25689  itg2const2  25710  itg2splitlem  25717  itg2split  25718  itg2cnlem1  25730  itg2cnlem2  25731  iblss2  25775  itgspliticc  25806  ditgpos  25825  limcres  25855  plyeq0lem  26183  plypf1  26185  coeeq2  26215  dvply1  26259  aareccl  26302  dvtaylp  26346  pserdvlem2  26406  lgamgulmlem4  27010  isppw  27092  vmappw  27094  muval1  27111  dchrelbasd  27218  dchr1  27236  dchrptlem2  27244  lgsdir2  27309  lgsne0  27314  gausslemma2dlem1a  27344  gausslemma2dlem2  27346  2sqnn0  27417  rplogsumlem2  27464  dchrisum0flblem2  27488  dchrisum0fno1  27490  rplogsum  27506  pntrlog2bndlem5  27560  noinfbnd2  27711  expnnsval  28434  1loopgrvd2  29589  1hevtxdg1  29592  1egrvtxdg1  29595  crctcshwlkn0lem2  29896  crctcshlem4  29905  crctcsh  29909  clwlkclwwlklem2fv1  30082  eulercrct  30329  eucrct2eupth  30332  ccatws1f1o  33043  pmtridfv1  33188  pmtridfv2  33189  psgnfzto1stlem  33193  elrgspnlem2  33336  elrgspnlem3  33337  elrspunsn  33521  gsummoncoe1fzo  33689  evlextv  33718  esplyind  33751  vieta  33756  fldextrspunlsp  33851  extdgfialglem2  33870  rtelextdg2lem  33903  2sqr3minply  33957  smattl  33975  smattr  33976  smatbl  33977  1smat1  33981  madjusmdetlem1  34004  madjusmdetlem2  34005  esumpinfval  34250  eulerpartlemgs2  34557  ballotlemsgt1  34688  ballotlemsel1i  34690  ballotlemsi  34692  signswmnd  34734  signsvtn  34761  cvmliftlem10  35507  unblimceq0lem  36725  bj-rdg0gALT  37313  poimirlem1  37866  poimirlem2  37867  poimirlem5  37870  poimirlem6  37871  poimirlem12  37877  poimirlem17  37882  poimirlem19  37884  poimirlem20  37885  poimirlem22  37887  poimirlem23  37888  itg2addnc  37919  itg2gt0cn  37920  itgaddnclem2  37924  sdclem1  37988  cdlemefs27cl  40783  sticksstones9  42518  sticksstones10  42519  sticksstones12a  42521  unitscyglem1  42559  flcidc  43521  oe0suclim  43628  tfsconcatfv  43692  safesnsupfilb  43768  relexp01min  44063  relexpxpmin  44067  mnurnd  44633  ioondisj2  45847  ioondisj1  45848  lptioo1  45986  limsup10exlem  46124  icccncfext  46239  cncfiooicc  46246  ioodvbdlimc1lem2  46284  ioodvbdlimc2lem  46286  dvnxpaek  46294  ditgeq3d  46316  itgsubsticclem  46327  dirkerper  46448  dirkercncflem2  46456  fourierdlem40  46499  fourierdlem65  46523  fourierdlem74  46532  fourierdlem75  46533  fourierdlem78  46536  fourierdlem81  46539  fourierdlem97  46555  fourierdlem103  46561  fourierdlem104  46562  sqwvfoura  46580  sqwvfourb  46581  fourierswlem  46582  fouriersw  46583  elaa2lem  46585  etransclem19  46605  etransclem22  46608  etransclem24  46610  etransclem35  46621  sge0pnfval  46725  isomenndlem  46882  hoicvrrex  46908  ovn0  46918  volicon0  46927  hsphoidmvle2  46937  hsphoidmvle  46938  hoidmv1lelem1  46943  hoidmv1lelem2  46944  hoidmvlelem2  46948  hoidmvlelem3  46949  hspmbllem1  46978  hspmbllem2  46979  volico2  46993  ovolval2lem  46995  ovnsubadd2lem  46997  ovolval4lem1  47001  vonioolem1  47032  vonioo  47034  vonicclem1  47035  vonicc  47037  discsubc  49417  oppf1st2nd  49484  2oppf  49485  oppfval  49489